The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF).

(0) Obligation:

Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

#abs(#0) → #0
#abs(#neg(@x)) → #pos(@x)
#abs(#pos(@x)) → #pos(@x)
#abs(#s(@x)) → #pos(#s(@x))
#less(@x, @y) → #cklt(#compare(@x, @y))
insert(@x, @l) → insert#1(@l, @x)
insert#1(::(@y, @ys), @x) → insert#2(#less(@y, @x), @x, @y, @ys)
insert#1(nil, @x) → ::(@x, nil)
insert#2(#false, @x, @y, @ys) → ::(@x, ::(@y, @ys))
insert#2(#true, @x, @y, @ys) → ::(@y, insert(@x, @ys))
insertD(@x, @l) → insertD#1(@l, @x)
insertD#1(::(@y, @ys), @x) → insertD#2(#less(@y, @x), @x, @y, @ys)
insertD#1(nil, @x) → ::(@x, nil)
insertD#2(#false, @x, @y, @ys) → ::(@x, ::(@y, @ys))
insertD#2(#true, @x, @y, @ys) → ::(@y, insertD(@x, @ys))
insertionsort(@l) → insertionsort#1(@l)
insertionsort#1(::(@x, @xs)) → insert(@x, insertionsort(@xs))
insertionsort#1(nil) → nil
insertionsortD(@l) → insertionsortD#1(@l)
insertionsortD#1(::(@x, @xs)) → insertD(@x, insertionsortD(@xs))
insertionsortD#1(nil) → nil
testInsertionsort(@x) → insertionsort(testList(#unit))
testInsertionsortD(@x) → insertionsortD(testList(#unit))
testList(@_) → ::(#abs(#0), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0))))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#0))))))))), ::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0)))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#0)))))))), ::(#abs(#pos(#s(#s(#s(#0))))), nil))))))))))

The (relative) TRS S consists of the following rules:

#cklt(#EQ) → #false
#cklt(#GT) → #false
#cklt(#LT) → #true
#compare(#0, #0) → #EQ
#compare(#0, #neg(@y)) → #GT
#compare(#0, #pos(@y)) → #LT
#compare(#0, #s(@y)) → #LT
#compare(#neg(@x), #0) → #LT
#compare(#neg(@x), #neg(@y)) → #compare(@y, @x)
#compare(#neg(@x), #pos(@y)) → #LT
#compare(#pos(@x), #0) → #GT
#compare(#pos(@x), #neg(@y)) → #GT
#compare(#pos(@x), #pos(@y)) → #compare(@x, @y)
#compare(#s(@x), #0) → #GT
#compare(#s(@x), #s(@y)) → #compare(@x, @y)

Rewrite Strategy: INNERMOST

(1) RenamingProof (EQUIVALENT transformation)

Renamed function symbols to avoid clashes with predefined symbol.

(2) Obligation:

Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

#abs(#0) → #0
#abs(#neg(@x)) → #pos(@x)
#abs(#pos(@x)) → #pos(@x)
#abs(#s(@x)) → #pos(#s(@x))
#less(@x, @y) → #cklt(#compare(@x, @y))
insert(@x, @l) → insert#1(@l, @x)
insert#1(::(@y, @ys), @x) → insert#2(#less(@y, @x), @x, @y, @ys)
insert#1(nil, @x) → ::(@x, nil)
insert#2(#false, @x, @y, @ys) → ::(@x, ::(@y, @ys))
insert#2(#true, @x, @y, @ys) → ::(@y, insert(@x, @ys))
insertD(@x, @l) → insertD#1(@l, @x)
insertD#1(::(@y, @ys), @x) → insertD#2(#less(@y, @x), @x, @y, @ys)
insertD#1(nil, @x) → ::(@x, nil)
insertD#2(#false, @x, @y, @ys) → ::(@x, ::(@y, @ys))
insertD#2(#true, @x, @y, @ys) → ::(@y, insertD(@x, @ys))
insertionsort(@l) → insertionsort#1(@l)
insertionsort#1(::(@x, @xs)) → insert(@x, insertionsort(@xs))
insertionsort#1(nil) → nil
insertionsortD(@l) → insertionsortD#1(@l)
insertionsortD#1(::(@x, @xs)) → insertD(@x, insertionsortD(@xs))
insertionsortD#1(nil) → nil
testInsertionsort(@x) → insertionsort(testList(#unit))
testInsertionsortD(@x) → insertionsortD(testList(#unit))
testList(@_) → ::(#abs(#0), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0))))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#0))))))))), ::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0)))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#0)))))))), ::(#abs(#pos(#s(#s(#s(#0))))), nil))))))))))

The (relative) TRS S consists of the following rules:

#cklt(#EQ) → #false
#cklt(#GT) → #false
#cklt(#LT) → #true
#compare(#0, #0) → #EQ
#compare(#0, #neg(@y)) → #GT
#compare(#0, #pos(@y)) → #LT
#compare(#0, #s(@y)) → #LT
#compare(#neg(@x), #0) → #LT
#compare(#neg(@x), #neg(@y)) → #compare(@y, @x)
#compare(#neg(@x), #pos(@y)) → #LT
#compare(#pos(@x), #0) → #GT
#compare(#pos(@x), #neg(@y)) → #GT
#compare(#pos(@x), #pos(@y)) → #compare(@x, @y)
#compare(#s(@x), #0) → #GT
#compare(#s(@x), #s(@y)) → #compare(@x, @y)

Rewrite Strategy: INNERMOST

(3) SlicingProof (LOWER BOUND(ID) transformation)

Sliced the following arguments:
testInsertionsort/0
testList/0
testInsertionsortD/0

(4) Obligation:

Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

#abs(#0) → #0
#abs(#neg(@x)) → #pos(@x)
#abs(#pos(@x)) → #pos(@x)
#abs(#s(@x)) → #pos(#s(@x))
#less(@x, @y) → #cklt(#compare(@x, @y))
insert(@x, @l) → insert#1(@l, @x)
insert#1(::(@y, @ys), @x) → insert#2(#less(@y, @x), @x, @y, @ys)
insert#1(nil, @x) → ::(@x, nil)
insert#2(#false, @x, @y, @ys) → ::(@x, ::(@y, @ys))
insert#2(#true, @x, @y, @ys) → ::(@y, insert(@x, @ys))
insertD(@x, @l) → insertD#1(@l, @x)
insertD#1(::(@y, @ys), @x) → insertD#2(#less(@y, @x), @x, @y, @ys)
insertD#1(nil, @x) → ::(@x, nil)
insertD#2(#false, @x, @y, @ys) → ::(@x, ::(@y, @ys))
insertD#2(#true, @x, @y, @ys) → ::(@y, insertD(@x, @ys))
insertionsort(@l) → insertionsort#1(@l)
insertionsort#1(::(@x, @xs)) → insert(@x, insertionsort(@xs))
insertionsort#1(nil) → nil
insertionsortD(@l) → insertionsortD#1(@l)
insertionsortD#1(::(@x, @xs)) → insertD(@x, insertionsortD(@xs))
insertionsortD#1(nil) → nil
testInsertionsort → insertionsort(testList)
testInsertionsortD → insertionsortD(testList)
testList → ::(#abs(#0), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0))))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#0))))))))), ::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0)))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#0)))))))), ::(#abs(#pos(#s(#s(#s(#0))))), nil))))))))))

The (relative) TRS S consists of the following rules:

#cklt(#EQ) → #false
#cklt(#GT) → #false
#cklt(#LT) → #true
#compare(#0, #0) → #EQ
#compare(#0, #neg(@y)) → #GT
#compare(#0, #pos(@y)) → #LT
#compare(#0, #s(@y)) → #LT
#compare(#neg(@x), #0) → #LT
#compare(#neg(@x), #neg(@y)) → #compare(@y, @x)
#compare(#neg(@x), #pos(@y)) → #LT
#compare(#pos(@x), #0) → #GT
#compare(#pos(@x), #neg(@y)) → #GT
#compare(#pos(@x), #pos(@y)) → #compare(@x, @y)
#compare(#s(@x), #0) → #GT
#compare(#s(@x), #s(@y)) → #compare(@x, @y)

Rewrite Strategy: INNERMOST

(5) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)

Infered types.

(6) Obligation:

Innermost TRS:
Rules:
#abs(#0) → #0
#abs(#neg(@x)) → #pos(@x)
#abs(#pos(@x)) → #pos(@x)
#abs(#s(@x)) → #pos(#s(@x))
#less(@x, @y) → #cklt(#compare(@x, @y))
insert(@x, @l) → insert#1(@l, @x)
insert#1(::(@y, @ys), @x) → insert#2(#less(@y, @x), @x, @y, @ys)
insert#1(nil, @x) → ::(@x, nil)
insert#2(#false, @x, @y, @ys) → ::(@x, ::(@y, @ys))
insert#2(#true, @x, @y, @ys) → ::(@y, insert(@x, @ys))
insertD(@x, @l) → insertD#1(@l, @x)
insertD#1(::(@y, @ys), @x) → insertD#2(#less(@y, @x), @x, @y, @ys)
insertD#1(nil, @x) → ::(@x, nil)
insertD#2(#false, @x, @y, @ys) → ::(@x, ::(@y, @ys))
insertD#2(#true, @x, @y, @ys) → ::(@y, insertD(@x, @ys))
insertionsort(@l) → insertionsort#1(@l)
insertionsort#1(::(@x, @xs)) → insert(@x, insertionsort(@xs))
insertionsort#1(nil) → nil
insertionsortD(@l) → insertionsortD#1(@l)
insertionsortD#1(::(@x, @xs)) → insertD(@x, insertionsortD(@xs))
insertionsortD#1(nil) → nil
testInsertionsort → insertionsort(testList)
testInsertionsortD → insertionsortD(testList)
testList → ::(#abs(#0), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0))))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#0))))))))), ::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0)))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#0)))))))), ::(#abs(#pos(#s(#s(#s(#0))))), nil))))))))))
#cklt(#EQ) → #false
#cklt(#GT) → #false
#cklt(#LT) → #true
#compare(#0, #0) → #EQ
#compare(#0, #neg(@y)) → #GT
#compare(#0, #pos(@y)) → #LT
#compare(#0, #s(@y)) → #LT
#compare(#neg(@x), #0) → #LT
#compare(#neg(@x), #neg(@y)) → #compare(@y, @x)
#compare(#neg(@x), #pos(@y)) → #LT
#compare(#pos(@x), #0) → #GT
#compare(#pos(@x), #neg(@y)) → #GT
#compare(#pos(@x), #pos(@y)) → #compare(@x, @y)
#compare(#s(@x), #0) → #GT
#compare(#s(@x), #s(@y)) → #compare(@x, @y)

Types:
#abs :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#0 :: #0:#neg:#pos:#s
#neg :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#pos :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#s :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#less :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
#compare :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #EQ:#GT:#LT
insert :: #0:#neg:#pos:#s → :::nil → :::nil
insert#1 :: :::nil → #0:#neg:#pos:#s → :::nil
:: :: #0:#neg:#pos:#s → :::nil → :::nil
insert#2 :: #false:#true → #0:#neg:#pos:#s → #0:#neg:#pos:#s → :::nil → :::nil
nil :: :::nil
#false :: #false:#true
#true :: #false:#true
insertD :: #0:#neg:#pos:#s → :::nil → :::nil
insertD#1 :: :::nil → #0:#neg:#pos:#s → :::nil
insertD#2 :: #false:#true → #0:#neg:#pos:#s → #0:#neg:#pos:#s → :::nil → :::nil
insertionsort :: :::nil → :::nil
insertionsort#1 :: :::nil → :::nil
insertionsortD :: :::nil → :::nil
insertionsortD#1 :: :::nil → :::nil
testInsertionsort :: :::nil
testList :: :::nil
testInsertionsortD :: :::nil
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
hole_#0:#neg:#pos:#s1_3 :: #0:#neg:#pos:#s
hole_#false:#true2_3 :: #false:#true
hole_#EQ:#GT:#LT3_3 :: #EQ:#GT:#LT
hole_:::nil4_3 :: :::nil
gen_#0:#neg:#pos:#s5_3 :: Nat → #0:#neg:#pos:#s
gen_:::nil6_3 :: Nat → :::nil

(7) OrderProof (LOWER BOUND(ID) transformation)

Heuristically decided to analyse the following defined symbols:
#compare, insert, insert#1, insertD, insertD#1, insertionsort, insertionsort#1, insertionsortD, insertionsortD#1

They will be analysed ascendingly in the following order:
insert = insert#1
insert < insertionsort#1
insertD = insertD#1
insertD < insertionsortD#1
insertionsort = insertionsort#1
insertionsortD = insertionsortD#1

(8) Obligation:

Innermost TRS:
Rules:
#abs(#0) → #0
#abs(#neg(@x)) → #pos(@x)
#abs(#pos(@x)) → #pos(@x)
#abs(#s(@x)) → #pos(#s(@x))
#less(@x, @y) → #cklt(#compare(@x, @y))
insert(@x, @l) → insert#1(@l, @x)
insert#1(::(@y, @ys), @x) → insert#2(#less(@y, @x), @x, @y, @ys)
insert#1(nil, @x) → ::(@x, nil)
insert#2(#false, @x, @y, @ys) → ::(@x, ::(@y, @ys))
insert#2(#true, @x, @y, @ys) → ::(@y, insert(@x, @ys))
insertD(@x, @l) → insertD#1(@l, @x)
insertD#1(::(@y, @ys), @x) → insertD#2(#less(@y, @x), @x, @y, @ys)
insertD#1(nil, @x) → ::(@x, nil)
insertD#2(#false, @x, @y, @ys) → ::(@x, ::(@y, @ys))
insertD#2(#true, @x, @y, @ys) → ::(@y, insertD(@x, @ys))
insertionsort(@l) → insertionsort#1(@l)
insertionsort#1(::(@x, @xs)) → insert(@x, insertionsort(@xs))
insertionsort#1(nil) → nil
insertionsortD(@l) → insertionsortD#1(@l)
insertionsortD#1(::(@x, @xs)) → insertD(@x, insertionsortD(@xs))
insertionsortD#1(nil) → nil
testInsertionsort → insertionsort(testList)
testInsertionsortD → insertionsortD(testList)
testList → ::(#abs(#0), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0))))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#0))))))))), ::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0)))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#0)))))))), ::(#abs(#pos(#s(#s(#s(#0))))), nil))))))))))
#cklt(#EQ) → #false
#cklt(#GT) → #false
#cklt(#LT) → #true
#compare(#0, #0) → #EQ
#compare(#0, #neg(@y)) → #GT
#compare(#0, #pos(@y)) → #LT
#compare(#0, #s(@y)) → #LT
#compare(#neg(@x), #0) → #LT
#compare(#neg(@x), #neg(@y)) → #compare(@y, @x)
#compare(#neg(@x), #pos(@y)) → #LT
#compare(#pos(@x), #0) → #GT
#compare(#pos(@x), #neg(@y)) → #GT
#compare(#pos(@x), #pos(@y)) → #compare(@x, @y)
#compare(#s(@x), #0) → #GT
#compare(#s(@x), #s(@y)) → #compare(@x, @y)

Types:
#abs :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#0 :: #0:#neg:#pos:#s
#neg :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#pos :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#s :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#less :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
#compare :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #EQ:#GT:#LT
insert :: #0:#neg:#pos:#s → :::nil → :::nil
insert#1 :: :::nil → #0:#neg:#pos:#s → :::nil
:: :: #0:#neg:#pos:#s → :::nil → :::nil
insert#2 :: #false:#true → #0:#neg:#pos:#s → #0:#neg:#pos:#s → :::nil → :::nil
nil :: :::nil
#false :: #false:#true
#true :: #false:#true
insertD :: #0:#neg:#pos:#s → :::nil → :::nil
insertD#1 :: :::nil → #0:#neg:#pos:#s → :::nil
insertD#2 :: #false:#true → #0:#neg:#pos:#s → #0:#neg:#pos:#s → :::nil → :::nil
insertionsort :: :::nil → :::nil
insertionsort#1 :: :::nil → :::nil
insertionsortD :: :::nil → :::nil
insertionsortD#1 :: :::nil → :::nil
testInsertionsort :: :::nil
testList :: :::nil
testInsertionsortD :: :::nil
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
hole_#0:#neg:#pos:#s1_3 :: #0:#neg:#pos:#s
hole_#false:#true2_3 :: #false:#true
hole_#EQ:#GT:#LT3_3 :: #EQ:#GT:#LT
hole_:::nil4_3 :: :::nil
gen_#0:#neg:#pos:#s5_3 :: Nat → #0:#neg:#pos:#s
gen_:::nil6_3 :: Nat → :::nil

Generator Equations:
gen_#0:#neg:#pos:#s5_3(0) ⇔ #0
gen_#0:#neg:#pos:#s5_3(+(x, 1)) ⇔ #neg(gen_#0:#neg:#pos:#s5_3(x))
gen_:::nil6_3(0) ⇔ nil
gen_:::nil6_3(+(x, 1)) ⇔ ::(#0, gen_:::nil6_3(x))

The following defined symbols remain to be analysed:
#compare, insert, insert#1, insertD, insertD#1, insertionsort, insertionsort#1, insertionsortD, insertionsortD#1

They will be analysed ascendingly in the following order:
insert = insert#1
insert < insertionsort#1
insertD = insertD#1
insertD < insertionsortD#1
insertionsort = insertionsort#1
insertionsortD = insertionsortD#1

(9) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
#compare(gen_#0:#neg:#pos:#s5_3(n8_3), gen_#0:#neg:#pos:#s5_3(n8_3)) → #EQ, rt ∈ Ω(0)

Induction Base:
#compare(gen_#0:#neg:#pos:#s5_3(0), gen_#0:#neg:#pos:#s5_3(0)) →_R^Ω(0)
#EQ

Induction Step:
#compare(gen_#0:#neg:#pos:#s5_3(+(n8_3, 1)), gen_#0:#neg:#pos:#s5_3(+(n8_3, 1))) →_R^Ω(0)
#compare(gen_#0:#neg:#pos:#s5_3(n8_3), gen_#0:#neg:#pos:#s5_3(n8_3)) →_IH
#EQ

We have rt ∈ Ω(1) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n⁰).

(10) Complex Obligation (BEST)

(11) Obligation:

Innermost TRS:
Rules:
#abs(#0) → #0
#abs(#neg(@x)) → #pos(@x)
#abs(#pos(@x)) → #pos(@x)
#abs(#s(@x)) → #pos(#s(@x))
#less(@x, @y) → #cklt(#compare(@x, @y))
insert(@x, @l) → insert#1(@l, @x)
insert#1(::(@y, @ys), @x) → insert#2(#less(@y, @x), @x, @y, @ys)
insert#1(nil, @x) → ::(@x, nil)
insert#2(#false, @x, @y, @ys) → ::(@x, ::(@y, @ys))
insert#2(#true, @x, @y, @ys) → ::(@y, insert(@x, @ys))
insertD(@x, @l) → insertD#1(@l, @x)
insertD#1(::(@y, @ys), @x) → insertD#2(#less(@y, @x), @x, @y, @ys)
insertD#1(nil, @x) → ::(@x, nil)
insertD#2(#false, @x, @y, @ys) → ::(@x, ::(@y, @ys))
insertD#2(#true, @x, @y, @ys) → ::(@y, insertD(@x, @ys))
insertionsort(@l) → insertionsort#1(@l)
insertionsort#1(::(@x, @xs)) → insert(@x, insertionsort(@xs))
insertionsort#1(nil) → nil
insertionsortD(@l) → insertionsortD#1(@l)
insertionsortD#1(::(@x, @xs)) → insertD(@x, insertionsortD(@xs))
insertionsortD#1(nil) → nil
testInsertionsort → insertionsort(testList)
testInsertionsortD → insertionsortD(testList)
testList → ::(#abs(#0), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0))))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#0))))))))), ::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0)))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#0)))))))), ::(#abs(#pos(#s(#s(#s(#0))))), nil))))))))))
#cklt(#EQ) → #false
#cklt(#GT) → #false
#cklt(#LT) → #true
#compare(#0, #0) → #EQ
#compare(#0, #neg(@y)) → #GT
#compare(#0, #pos(@y)) → #LT
#compare(#0, #s(@y)) → #LT
#compare(#neg(@x), #0) → #LT
#compare(#neg(@x), #neg(@y)) → #compare(@y, @x)
#compare(#neg(@x), #pos(@y)) → #LT
#compare(#pos(@x), #0) → #GT
#compare(#pos(@x), #neg(@y)) → #GT
#compare(#pos(@x), #pos(@y)) → #compare(@x, @y)
#compare(#s(@x), #0) → #GT
#compare(#s(@x), #s(@y)) → #compare(@x, @y)

Types:
#abs :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#0 :: #0:#neg:#pos:#s
#neg :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#pos :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#s :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#less :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
#compare :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #EQ:#GT:#LT
insert :: #0:#neg:#pos:#s → :::nil → :::nil
insert#1 :: :::nil → #0:#neg:#pos:#s → :::nil
:: :: #0:#neg:#pos:#s → :::nil → :::nil
insert#2 :: #false:#true → #0:#neg:#pos:#s → #0:#neg:#pos:#s → :::nil → :::nil
nil :: :::nil
#false :: #false:#true
#true :: #false:#true
insertD :: #0:#neg:#pos:#s → :::nil → :::nil
insertD#1 :: :::nil → #0:#neg:#pos:#s → :::nil
insertD#2 :: #false:#true → #0:#neg:#pos:#s → #0:#neg:#pos:#s → :::nil → :::nil
insertionsort :: :::nil → :::nil
insertionsort#1 :: :::nil → :::nil
insertionsortD :: :::nil → :::nil
insertionsortD#1 :: :::nil → :::nil
testInsertionsort :: :::nil
testList :: :::nil
testInsertionsortD :: :::nil
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
hole_#0:#neg:#pos:#s1_3 :: #0:#neg:#pos:#s
hole_#false:#true2_3 :: #false:#true
hole_#EQ:#GT:#LT3_3 :: #EQ:#GT:#LT
hole_:::nil4_3 :: :::nil
gen_#0:#neg:#pos:#s5_3 :: Nat → #0:#neg:#pos:#s
gen_:::nil6_3 :: Nat → :::nil

Lemmas:
#compare(gen_#0:#neg:#pos:#s5_3(n8_3), gen_#0:#neg:#pos:#s5_3(n8_3)) → #EQ, rt ∈ Ω(0)

Generator Equations:
gen_#0:#neg:#pos:#s5_3(0) ⇔ #0
gen_#0:#neg:#pos:#s5_3(+(x, 1)) ⇔ #neg(gen_#0:#neg:#pos:#s5_3(x))
gen_:::nil6_3(0) ⇔ nil
gen_:::nil6_3(+(x, 1)) ⇔ ::(#0, gen_:::nil6_3(x))

The following defined symbols remain to be analysed:
insertD#1, insert, insert#1, insertD, insertionsort, insertionsort#1, insertionsortD, insertionsortD#1

They will be analysed ascendingly in the following order:
insert = insert#1
insert < insertionsort#1
insertD = insertD#1
insertD < insertionsortD#1
insertionsort = insertionsort#1
insertionsortD = insertionsortD#1

(12) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol insertD#1.

(13) Obligation:

Innermost TRS:
Rules:
#abs(#0) → #0
#abs(#neg(@x)) → #pos(@x)
#abs(#pos(@x)) → #pos(@x)
#abs(#s(@x)) → #pos(#s(@x))
#less(@x, @y) → #cklt(#compare(@x, @y))
insert(@x, @l) → insert#1(@l, @x)
insert#1(::(@y, @ys), @x) → insert#2(#less(@y, @x), @x, @y, @ys)
insert#1(nil, @x) → ::(@x, nil)
insert#2(#false, @x, @y, @ys) → ::(@x, ::(@y, @ys))
insert#2(#true, @x, @y, @ys) → ::(@y, insert(@x, @ys))
insertD(@x, @l) → insertD#1(@l, @x)
insertD#1(::(@y, @ys), @x) → insertD#2(#less(@y, @x), @x, @y, @ys)
insertD#1(nil, @x) → ::(@x, nil)
insertD#2(#false, @x, @y, @ys) → ::(@x, ::(@y, @ys))
insertD#2(#true, @x, @y, @ys) → ::(@y, insertD(@x, @ys))
insertionsort(@l) → insertionsort#1(@l)
insertionsort#1(::(@x, @xs)) → insert(@x, insertionsort(@xs))
insertionsort#1(nil) → nil
insertionsortD(@l) → insertionsortD#1(@l)
insertionsortD#1(::(@x, @xs)) → insertD(@x, insertionsortD(@xs))
insertionsortD#1(nil) → nil
testInsertionsort → insertionsort(testList)
testInsertionsortD → insertionsortD(testList)
testList → ::(#abs(#0), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0))))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#0))))))))), ::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0)))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#0)))))))), ::(#abs(#pos(#s(#s(#s(#0))))), nil))))))))))
#cklt(#EQ) → #false
#cklt(#GT) → #false
#cklt(#LT) → #true
#compare(#0, #0) → #EQ
#compare(#0, #neg(@y)) → #GT
#compare(#0, #pos(@y)) → #LT
#compare(#0, #s(@y)) → #LT
#compare(#neg(@x), #0) → #LT
#compare(#neg(@x), #neg(@y)) → #compare(@y, @x)
#compare(#neg(@x), #pos(@y)) → #LT
#compare(#pos(@x), #0) → #GT
#compare(#pos(@x), #neg(@y)) → #GT
#compare(#pos(@x), #pos(@y)) → #compare(@x, @y)
#compare(#s(@x), #0) → #GT
#compare(#s(@x), #s(@y)) → #compare(@x, @y)

Types:
#abs :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#0 :: #0:#neg:#pos:#s
#neg :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#pos :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#s :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#less :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
#compare :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #EQ:#GT:#LT
insert :: #0:#neg:#pos:#s → :::nil → :::nil
insert#1 :: :::nil → #0:#neg:#pos:#s → :::nil
:: :: #0:#neg:#pos:#s → :::nil → :::nil
insert#2 :: #false:#true → #0:#neg:#pos:#s → #0:#neg:#pos:#s → :::nil → :::nil
nil :: :::nil
#false :: #false:#true
#true :: #false:#true
insertD :: #0:#neg:#pos:#s → :::nil → :::nil
insertD#1 :: :::nil → #0:#neg:#pos:#s → :::nil
insertD#2 :: #false:#true → #0:#neg:#pos:#s → #0:#neg:#pos:#s → :::nil → :::nil
insertionsort :: :::nil → :::nil
insertionsort#1 :: :::nil → :::nil
insertionsortD :: :::nil → :::nil
insertionsortD#1 :: :::nil → :::nil
testInsertionsort :: :::nil
testList :: :::nil
testInsertionsortD :: :::nil
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
hole_#0:#neg:#pos:#s1_3 :: #0:#neg:#pos:#s
hole_#false:#true2_3 :: #false:#true
hole_#EQ:#GT:#LT3_3 :: #EQ:#GT:#LT
hole_:::nil4_3 :: :::nil
gen_#0:#neg:#pos:#s5_3 :: Nat → #0:#neg:#pos:#s
gen_:::nil6_3 :: Nat → :::nil

Lemmas:
#compare(gen_#0:#neg:#pos:#s5_3(n8_3), gen_#0:#neg:#pos:#s5_3(n8_3)) → #EQ, rt ∈ Ω(0)

Generator Equations:
gen_#0:#neg:#pos:#s5_3(0) ⇔ #0
gen_#0:#neg:#pos:#s5_3(+(x, 1)) ⇔ #neg(gen_#0:#neg:#pos:#s5_3(x))
gen_:::nil6_3(0) ⇔ nil
gen_:::nil6_3(+(x, 1)) ⇔ ::(#0, gen_:::nil6_3(x))

The following defined symbols remain to be analysed:
insertD, insert, insert#1, insertionsort, insertionsort#1, insertionsortD, insertionsortD#1

They will be analysed ascendingly in the following order:
insert = insert#1
insert < insertionsort#1
insertD = insertD#1
insertD < insertionsortD#1
insertionsort = insertionsort#1
insertionsortD = insertionsortD#1

(14) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol insertD.

(15) Obligation:

Innermost TRS:
Rules:
#abs(#0) → #0
#abs(#neg(@x)) → #pos(@x)
#abs(#pos(@x)) → #pos(@x)
#abs(#s(@x)) → #pos(#s(@x))
#less(@x, @y) → #cklt(#compare(@x, @y))
insert(@x, @l) → insert#1(@l, @x)
insert#1(::(@y, @ys), @x) → insert#2(#less(@y, @x), @x, @y, @ys)
insert#1(nil, @x) → ::(@x, nil)
insert#2(#false, @x, @y, @ys) → ::(@x, ::(@y, @ys))
insert#2(#true, @x, @y, @ys) → ::(@y, insert(@x, @ys))
insertD(@x, @l) → insertD#1(@l, @x)
insertD#1(::(@y, @ys), @x) → insertD#2(#less(@y, @x), @x, @y, @ys)
insertD#1(nil, @x) → ::(@x, nil)
insertD#2(#false, @x, @y, @ys) → ::(@x, ::(@y, @ys))
insertD#2(#true, @x, @y, @ys) → ::(@y, insertD(@x, @ys))
insertionsort(@l) → insertionsort#1(@l)
insertionsort#1(::(@x, @xs)) → insert(@x, insertionsort(@xs))
insertionsort#1(nil) → nil
insertionsortD(@l) → insertionsortD#1(@l)
insertionsortD#1(::(@x, @xs)) → insertD(@x, insertionsortD(@xs))
insertionsortD#1(nil) → nil
testInsertionsort → insertionsort(testList)
testInsertionsortD → insertionsortD(testList)
testList → ::(#abs(#0), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0))))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#0))))))))), ::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0)))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#0)))))))), ::(#abs(#pos(#s(#s(#s(#0))))), nil))))))))))
#cklt(#EQ) → #false
#cklt(#GT) → #false
#cklt(#LT) → #true
#compare(#0, #0) → #EQ
#compare(#0, #neg(@y)) → #GT
#compare(#0, #pos(@y)) → #LT
#compare(#0, #s(@y)) → #LT
#compare(#neg(@x), #0) → #LT
#compare(#neg(@x), #neg(@y)) → #compare(@y, @x)
#compare(#neg(@x), #pos(@y)) → #LT
#compare(#pos(@x), #0) → #GT
#compare(#pos(@x), #neg(@y)) → #GT
#compare(#pos(@x), #pos(@y)) → #compare(@x, @y)
#compare(#s(@x), #0) → #GT
#compare(#s(@x), #s(@y)) → #compare(@x, @y)

Types:
#abs :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#0 :: #0:#neg:#pos:#s
#neg :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#pos :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#s :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#less :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
#compare :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #EQ:#GT:#LT
insert :: #0:#neg:#pos:#s → :::nil → :::nil
insert#1 :: :::nil → #0:#neg:#pos:#s → :::nil
:: :: #0:#neg:#pos:#s → :::nil → :::nil
insert#2 :: #false:#true → #0:#neg:#pos:#s → #0:#neg:#pos:#s → :::nil → :::nil
nil :: :::nil
#false :: #false:#true
#true :: #false:#true
insertD :: #0:#neg:#pos:#s → :::nil → :::nil
insertD#1 :: :::nil → #0:#neg:#pos:#s → :::nil
insertD#2 :: #false:#true → #0:#neg:#pos:#s → #0:#neg:#pos:#s → :::nil → :::nil
insertionsort :: :::nil → :::nil
insertionsort#1 :: :::nil → :::nil
insertionsortD :: :::nil → :::nil
insertionsortD#1 :: :::nil → :::nil
testInsertionsort :: :::nil
testList :: :::nil
testInsertionsortD :: :::nil
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
hole_#0:#neg:#pos:#s1_3 :: #0:#neg:#pos:#s
hole_#false:#true2_3 :: #false:#true
hole_#EQ:#GT:#LT3_3 :: #EQ:#GT:#LT
hole_:::nil4_3 :: :::nil
gen_#0:#neg:#pos:#s5_3 :: Nat → #0:#neg:#pos:#s
gen_:::nil6_3 :: Nat → :::nil

Lemmas:
#compare(gen_#0:#neg:#pos:#s5_3(n8_3), gen_#0:#neg:#pos:#s5_3(n8_3)) → #EQ, rt ∈ Ω(0)

Generator Equations:
gen_#0:#neg:#pos:#s5_3(0) ⇔ #0
gen_#0:#neg:#pos:#s5_3(+(x, 1)) ⇔ #neg(gen_#0:#neg:#pos:#s5_3(x))
gen_:::nil6_3(0) ⇔ nil
gen_:::nil6_3(+(x, 1)) ⇔ ::(#0, gen_:::nil6_3(x))

The following defined symbols remain to be analysed:
insertionsortD#1, insert, insert#1, insertionsort, insertionsort#1, insertionsortD

They will be analysed ascendingly in the following order:
insert = insert#1
insert < insertionsort#1
insertionsort = insertionsort#1
insertionsortD = insertionsortD#1

(16) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
insertionsortD#1(gen_:::nil6_3(n319337_3)) → *7_3, rt ∈ Ω(n319337₃)

Induction Base:
insertionsortD#1(gen_:::nil6_3(0))

Induction Step:
insertionsortD#1(gen_:::nil6_3(+(n319337_3, 1))) →_R^Ω(1)
insertD(#0, insertionsortD(gen_:::nil6_3(n319337_3))) →_R^Ω(1)
insertD(#0, insertionsortD#1(gen_:::nil6_3(n319337_3))) →_IH
insertD(#0, *7_3)

We have rt ∈ Ω(n¹) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

(17) Complex Obligation (BEST)

(18) Obligation:

Innermost TRS:
Rules:
#abs(#0) → #0
#abs(#neg(@x)) → #pos(@x)
#abs(#pos(@x)) → #pos(@x)
#abs(#s(@x)) → #pos(#s(@x))
#less(@x, @y) → #cklt(#compare(@x, @y))
insert(@x, @l) → insert#1(@l, @x)
insert#1(::(@y, @ys), @x) → insert#2(#less(@y, @x), @x, @y, @ys)
insert#1(nil, @x) → ::(@x, nil)
insert#2(#false, @x, @y, @ys) → ::(@x, ::(@y, @ys))
insert#2(#true, @x, @y, @ys) → ::(@y, insert(@x, @ys))
insertD(@x, @l) → insertD#1(@l, @x)
insertD#1(::(@y, @ys), @x) → insertD#2(#less(@y, @x), @x, @y, @ys)
insertD#1(nil, @x) → ::(@x, nil)
insertD#2(#false, @x, @y, @ys) → ::(@x, ::(@y, @ys))
insertD#2(#true, @x, @y, @ys) → ::(@y, insertD(@x, @ys))
insertionsort(@l) → insertionsort#1(@l)
insertionsort#1(::(@x, @xs)) → insert(@x, insertionsort(@xs))
insertionsort#1(nil) → nil
insertionsortD(@l) → insertionsortD#1(@l)
insertionsortD#1(::(@x, @xs)) → insertD(@x, insertionsortD(@xs))
insertionsortD#1(nil) → nil
testInsertionsort → insertionsort(testList)
testInsertionsortD → insertionsortD(testList)
testList → ::(#abs(#0), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0))))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#0))))))))), ::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0)))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#0)))))))), ::(#abs(#pos(#s(#s(#s(#0))))), nil))))))))))
#cklt(#EQ) → #false
#cklt(#GT) → #false
#cklt(#LT) → #true
#compare(#0, #0) → #EQ
#compare(#0, #neg(@y)) → #GT
#compare(#0, #pos(@y)) → #LT
#compare(#0, #s(@y)) → #LT
#compare(#neg(@x), #0) → #LT
#compare(#neg(@x), #neg(@y)) → #compare(@y, @x)
#compare(#neg(@x), #pos(@y)) → #LT
#compare(#pos(@x), #0) → #GT
#compare(#pos(@x), #neg(@y)) → #GT
#compare(#pos(@x), #pos(@y)) → #compare(@x, @y)
#compare(#s(@x), #0) → #GT
#compare(#s(@x), #s(@y)) → #compare(@x, @y)

Types:
#abs :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#0 :: #0:#neg:#pos:#s
#neg :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#pos :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#s :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#less :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
#compare :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #EQ:#GT:#LT
insert :: #0:#neg:#pos:#s → :::nil → :::nil
insert#1 :: :::nil → #0:#neg:#pos:#s → :::nil
:: :: #0:#neg:#pos:#s → :::nil → :::nil
insert#2 :: #false:#true → #0:#neg:#pos:#s → #0:#neg:#pos:#s → :::nil → :::nil
nil :: :::nil
#false :: #false:#true
#true :: #false:#true
insertD :: #0:#neg:#pos:#s → :::nil → :::nil
insertD#1 :: :::nil → #0:#neg:#pos:#s → :::nil
insertD#2 :: #false:#true → #0:#neg:#pos:#s → #0:#neg:#pos:#s → :::nil → :::nil
insertionsort :: :::nil → :::nil
insertionsort#1 :: :::nil → :::nil
insertionsortD :: :::nil → :::nil
insertionsortD#1 :: :::nil → :::nil
testInsertionsort :: :::nil
testList :: :::nil
testInsertionsortD :: :::nil
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
hole_#0:#neg:#pos:#s1_3 :: #0:#neg:#pos:#s
hole_#false:#true2_3 :: #false:#true
hole_#EQ:#GT:#LT3_3 :: #EQ:#GT:#LT
hole_:::nil4_3 :: :::nil
gen_#0:#neg:#pos:#s5_3 :: Nat → #0:#neg:#pos:#s
gen_:::nil6_3 :: Nat → :::nil

Lemmas:
#compare(gen_#0:#neg:#pos:#s5_3(n8_3), gen_#0:#neg:#pos:#s5_3(n8_3)) → #EQ, rt ∈ Ω(0)
insertionsortD#1(gen_:::nil6_3(n319337_3)) → *7_3, rt ∈ Ω(n319337₃)

Generator Equations:
gen_#0:#neg:#pos:#s5_3(0) ⇔ #0
gen_#0:#neg:#pos:#s5_3(+(x, 1)) ⇔ #neg(gen_#0:#neg:#pos:#s5_3(x))
gen_:::nil6_3(0) ⇔ nil
gen_:::nil6_3(+(x, 1)) ⇔ ::(#0, gen_:::nil6_3(x))

The following defined symbols remain to be analysed:
insertionsortD, insert, insert#1, insertionsort, insertionsort#1

They will be analysed ascendingly in the following order:
insert = insert#1
insert < insertionsort#1
insertionsort = insertionsort#1
insertionsortD = insertionsortD#1

(19) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
insertionsortD(gen_:::nil6_3(n322968_3)) → *7_3, rt ∈ Ω(n322968₃)

Induction Base:
insertionsortD(gen_:::nil6_3(0))

Induction Step:
insertionsortD(gen_:::nil6_3(+(n322968_3, 1))) →_R^Ω(1)
insertionsortD#1(gen_:::nil6_3(+(n322968_3, 1))) →_R^Ω(1)
insertD(#0, insertionsortD(gen_:::nil6_3(n322968_3))) →_IH
insertD(#0, *7_3)

We have rt ∈ Ω(n¹) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

(20) Complex Obligation (BEST)

(21) Obligation:

Innermost TRS:
Rules:
#abs(#0) → #0
#abs(#neg(@x)) → #pos(@x)
#abs(#pos(@x)) → #pos(@x)
#abs(#s(@x)) → #pos(#s(@x))
#less(@x, @y) → #cklt(#compare(@x, @y))
insert(@x, @l) → insert#1(@l, @x)
insert#1(::(@y, @ys), @x) → insert#2(#less(@y, @x), @x, @y, @ys)
insert#1(nil, @x) → ::(@x, nil)
insert#2(#false, @x, @y, @ys) → ::(@x, ::(@y, @ys))
insert#2(#true, @x, @y, @ys) → ::(@y, insert(@x, @ys))
insertD(@x, @l) → insertD#1(@l, @x)
insertD#1(::(@y, @ys), @x) → insertD#2(#less(@y, @x), @x, @y, @ys)
insertD#1(nil, @x) → ::(@x, nil)
insertD#2(#false, @x, @y, @ys) → ::(@x, ::(@y, @ys))
insertD#2(#true, @x, @y, @ys) → ::(@y, insertD(@x, @ys))
insertionsort(@l) → insertionsort#1(@l)
insertionsort#1(::(@x, @xs)) → insert(@x, insertionsort(@xs))
insertionsort#1(nil) → nil
insertionsortD(@l) → insertionsortD#1(@l)
insertionsortD#1(::(@x, @xs)) → insertD(@x, insertionsortD(@xs))
insertionsortD#1(nil) → nil
testInsertionsort → insertionsort(testList)
testInsertionsortD → insertionsortD(testList)
testList → ::(#abs(#0), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0))))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#0))))))))), ::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0)))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#0)))))))), ::(#abs(#pos(#s(#s(#s(#0))))), nil))))))))))
#cklt(#EQ) → #false
#cklt(#GT) → #false
#cklt(#LT) → #true
#compare(#0, #0) → #EQ
#compare(#0, #neg(@y)) → #GT
#compare(#0, #pos(@y)) → #LT
#compare(#0, #s(@y)) → #LT
#compare(#neg(@x), #0) → #LT
#compare(#neg(@x), #neg(@y)) → #compare(@y, @x)
#compare(#neg(@x), #pos(@y)) → #LT
#compare(#pos(@x), #0) → #GT
#compare(#pos(@x), #neg(@y)) → #GT
#compare(#pos(@x), #pos(@y)) → #compare(@x, @y)
#compare(#s(@x), #0) → #GT
#compare(#s(@x), #s(@y)) → #compare(@x, @y)

Types:
#abs :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#0 :: #0:#neg:#pos:#s
#neg :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#pos :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#s :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#less :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
#compare :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #EQ:#GT:#LT
insert :: #0:#neg:#pos:#s → :::nil → :::nil
insert#1 :: :::nil → #0:#neg:#pos:#s → :::nil
:: :: #0:#neg:#pos:#s → :::nil → :::nil
insert#2 :: #false:#true → #0:#neg:#pos:#s → #0:#neg:#pos:#s → :::nil → :::nil
nil :: :::nil
#false :: #false:#true
#true :: #false:#true
insertD :: #0:#neg:#pos:#s → :::nil → :::nil
insertD#1 :: :::nil → #0:#neg:#pos:#s → :::nil
insertD#2 :: #false:#true → #0:#neg:#pos:#s → #0:#neg:#pos:#s → :::nil → :::nil
insertionsort :: :::nil → :::nil
insertionsort#1 :: :::nil → :::nil
insertionsortD :: :::nil → :::nil
insertionsortD#1 :: :::nil → :::nil
testInsertionsort :: :::nil
testList :: :::nil
testInsertionsortD :: :::nil
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
hole_#0:#neg:#pos:#s1_3 :: #0:#neg:#pos:#s
hole_#false:#true2_3 :: #false:#true
hole_#EQ:#GT:#LT3_3 :: #EQ:#GT:#LT
hole_:::nil4_3 :: :::nil
gen_#0:#neg:#pos:#s5_3 :: Nat → #0:#neg:#pos:#s
gen_:::nil6_3 :: Nat → :::nil

Lemmas:
#compare(gen_#0:#neg:#pos:#s5_3(n8_3), gen_#0:#neg:#pos:#s5_3(n8_3)) → #EQ, rt ∈ Ω(0)
insertionsortD#1(gen_:::nil6_3(n319337_3)) → *7_3, rt ∈ Ω(n319337₃)
insertionsortD(gen_:::nil6_3(n322968_3)) → *7_3, rt ∈ Ω(n322968₃)

Generator Equations:
gen_#0:#neg:#pos:#s5_3(0) ⇔ #0
gen_#0:#neg:#pos:#s5_3(+(x, 1)) ⇔ #neg(gen_#0:#neg:#pos:#s5_3(x))
gen_:::nil6_3(0) ⇔ nil
gen_:::nil6_3(+(x, 1)) ⇔ ::(#0, gen_:::nil6_3(x))

The following defined symbols remain to be analysed:
insertionsortD#1, insert, insert#1, insertionsort, insertionsort#1

They will be analysed ascendingly in the following order:
insert = insert#1
insert < insertionsort#1
insertionsort = insertionsort#1
insertionsortD = insertionsortD#1

(22) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
insertionsortD#1(gen_:::nil6_3(n332039_3)) → *7_3, rt ∈ Ω(n332039₃)

Induction Base:
insertionsortD#1(gen_:::nil6_3(0))

Induction Step:
insertionsortD#1(gen_:::nil6_3(+(n332039_3, 1))) →_R^Ω(1)
insertD(#0, insertionsortD(gen_:::nil6_3(n332039_3))) →_R^Ω(1)
insertD(#0, insertionsortD#1(gen_:::nil6_3(n332039_3))) →_IH
insertD(#0, *7_3)

We have rt ∈ Ω(n¹) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

(23) Complex Obligation (BEST)

(24) Obligation:

Innermost TRS:
Rules:
#abs(#0) → #0
#abs(#neg(@x)) → #pos(@x)
#abs(#pos(@x)) → #pos(@x)
#abs(#s(@x)) → #pos(#s(@x))
#less(@x, @y) → #cklt(#compare(@x, @y))
insert(@x, @l) → insert#1(@l, @x)
insert#1(::(@y, @ys), @x) → insert#2(#less(@y, @x), @x, @y, @ys)
insert#1(nil, @x) → ::(@x, nil)
insert#2(#false, @x, @y, @ys) → ::(@x, ::(@y, @ys))
insert#2(#true, @x, @y, @ys) → ::(@y, insert(@x, @ys))
insertD(@x, @l) → insertD#1(@l, @x)
insertD#1(::(@y, @ys), @x) → insertD#2(#less(@y, @x), @x, @y, @ys)
insertD#1(nil, @x) → ::(@x, nil)
insertD#2(#false, @x, @y, @ys) → ::(@x, ::(@y, @ys))
insertD#2(#true, @x, @y, @ys) → ::(@y, insertD(@x, @ys))
insertionsort(@l) → insertionsort#1(@l)
insertionsort#1(::(@x, @xs)) → insert(@x, insertionsort(@xs))
insertionsort#1(nil) → nil
insertionsortD(@l) → insertionsortD#1(@l)
insertionsortD#1(::(@x, @xs)) → insertD(@x, insertionsortD(@xs))
insertionsortD#1(nil) → nil
testInsertionsort → insertionsort(testList)
testInsertionsortD → insertionsortD(testList)
testList → ::(#abs(#0), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0))))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#0))))))))), ::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0)))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#0)))))))), ::(#abs(#pos(#s(#s(#s(#0))))), nil))))))))))
#cklt(#EQ) → #false
#cklt(#GT) → #false
#cklt(#LT) → #true
#compare(#0, #0) → #EQ
#compare(#0, #neg(@y)) → #GT
#compare(#0, #pos(@y)) → #LT
#compare(#0, #s(@y)) → #LT
#compare(#neg(@x), #0) → #LT
#compare(#neg(@x), #neg(@y)) → #compare(@y, @x)
#compare(#neg(@x), #pos(@y)) → #LT
#compare(#pos(@x), #0) → #GT
#compare(#pos(@x), #neg(@y)) → #GT
#compare(#pos(@x), #pos(@y)) → #compare(@x, @y)
#compare(#s(@x), #0) → #GT
#compare(#s(@x), #s(@y)) → #compare(@x, @y)

Types:
#abs :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#0 :: #0:#neg:#pos:#s
#neg :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#pos :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#s :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#less :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
#compare :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #EQ:#GT:#LT
insert :: #0:#neg:#pos:#s → :::nil → :::nil
insert#1 :: :::nil → #0:#neg:#pos:#s → :::nil
:: :: #0:#neg:#pos:#s → :::nil → :::nil
insert#2 :: #false:#true → #0:#neg:#pos:#s → #0:#neg:#pos:#s → :::nil → :::nil
nil :: :::nil
#false :: #false:#true
#true :: #false:#true
insertD :: #0:#neg:#pos:#s → :::nil → :::nil
insertD#1 :: :::nil → #0:#neg:#pos:#s → :::nil
insertD#2 :: #false:#true → #0:#neg:#pos:#s → #0:#neg:#pos:#s → :::nil → :::nil
insertionsort :: :::nil → :::nil
insertionsort#1 :: :::nil → :::nil
insertionsortD :: :::nil → :::nil
insertionsortD#1 :: :::nil → :::nil
testInsertionsort :: :::nil
testList :: :::nil
testInsertionsortD :: :::nil
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
hole_#0:#neg:#pos:#s1_3 :: #0:#neg:#pos:#s
hole_#false:#true2_3 :: #false:#true
hole_#EQ:#GT:#LT3_3 :: #EQ:#GT:#LT
hole_:::nil4_3 :: :::nil
gen_#0:#neg:#pos:#s5_3 :: Nat → #0:#neg:#pos:#s
gen_:::nil6_3 :: Nat → :::nil

Lemmas:
#compare(gen_#0:#neg:#pos:#s5_3(n8_3), gen_#0:#neg:#pos:#s5_3(n8_3)) → #EQ, rt ∈ Ω(0)
insertionsortD#1(gen_:::nil6_3(n332039_3)) → *7_3, rt ∈ Ω(n332039₃)
insertionsortD(gen_:::nil6_3(n322968_3)) → *7_3, rt ∈ Ω(n322968₃)

Generator Equations:
gen_#0:#neg:#pos:#s5_3(0) ⇔ #0
gen_#0:#neg:#pos:#s5_3(+(x, 1)) ⇔ #neg(gen_#0:#neg:#pos:#s5_3(x))
gen_:::nil6_3(0) ⇔ nil
gen_:::nil6_3(+(x, 1)) ⇔ ::(#0, gen_:::nil6_3(x))

The following defined symbols remain to be analysed:
insert#1, insert, insertionsort, insertionsort#1

They will be analysed ascendingly in the following order:
insert = insert#1
insert < insertionsort#1
insertionsort = insertionsort#1

(25) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol insert#1.

(26) Obligation:

Innermost TRS:
Rules:
#abs(#0) → #0
#abs(#neg(@x)) → #pos(@x)
#abs(#pos(@x)) → #pos(@x)
#abs(#s(@x)) → #pos(#s(@x))
#less(@x, @y) → #cklt(#compare(@x, @y))
insert(@x, @l) → insert#1(@l, @x)
insert#1(::(@y, @ys), @x) → insert#2(#less(@y, @x), @x, @y, @ys)
insert#1(nil, @x) → ::(@x, nil)
insert#2(#false, @x, @y, @ys) → ::(@x, ::(@y, @ys))
insert#2(#true, @x, @y, @ys) → ::(@y, insert(@x, @ys))
insertD(@x, @l) → insertD#1(@l, @x)
insertD#1(::(@y, @ys), @x) → insertD#2(#less(@y, @x), @x, @y, @ys)
insertD#1(nil, @x) → ::(@x, nil)
insertD#2(#false, @x, @y, @ys) → ::(@x, ::(@y, @ys))
insertD#2(#true, @x, @y, @ys) → ::(@y, insertD(@x, @ys))
insertionsort(@l) → insertionsort#1(@l)
insertionsort#1(::(@x, @xs)) → insert(@x, insertionsort(@xs))
insertionsort#1(nil) → nil
insertionsortD(@l) → insertionsortD#1(@l)
insertionsortD#1(::(@x, @xs)) → insertD(@x, insertionsortD(@xs))
insertionsortD#1(nil) → nil
testInsertionsort → insertionsort(testList)
testInsertionsortD → insertionsortD(testList)
testList → ::(#abs(#0), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0))))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#0))))))))), ::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0)))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#0)))))))), ::(#abs(#pos(#s(#s(#s(#0))))), nil))))))))))
#cklt(#EQ) → #false
#cklt(#GT) → #false
#cklt(#LT) → #true
#compare(#0, #0) → #EQ
#compare(#0, #neg(@y)) → #GT
#compare(#0, #pos(@y)) → #LT
#compare(#0, #s(@y)) → #LT
#compare(#neg(@x), #0) → #LT
#compare(#neg(@x), #neg(@y)) → #compare(@y, @x)
#compare(#neg(@x), #pos(@y)) → #LT
#compare(#pos(@x), #0) → #GT
#compare(#pos(@x), #neg(@y)) → #GT
#compare(#pos(@x), #pos(@y)) → #compare(@x, @y)
#compare(#s(@x), #0) → #GT
#compare(#s(@x), #s(@y)) → #compare(@x, @y)

Types:
#abs :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#0 :: #0:#neg:#pos:#s
#neg :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#pos :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#s :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#less :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
#compare :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #EQ:#GT:#LT
insert :: #0:#neg:#pos:#s → :::nil → :::nil
insert#1 :: :::nil → #0:#neg:#pos:#s → :::nil
:: :: #0:#neg:#pos:#s → :::nil → :::nil
insert#2 :: #false:#true → #0:#neg:#pos:#s → #0:#neg:#pos:#s → :::nil → :::nil
nil :: :::nil
#false :: #false:#true
#true :: #false:#true
insertD :: #0:#neg:#pos:#s → :::nil → :::nil
insertD#1 :: :::nil → #0:#neg:#pos:#s → :::nil
insertD#2 :: #false:#true → #0:#neg:#pos:#s → #0:#neg:#pos:#s → :::nil → :::nil
insertionsort :: :::nil → :::nil
insertionsort#1 :: :::nil → :::nil
insertionsortD :: :::nil → :::nil
insertionsortD#1 :: :::nil → :::nil
testInsertionsort :: :::nil
testList :: :::nil
testInsertionsortD :: :::nil
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
hole_#0:#neg:#pos:#s1_3 :: #0:#neg:#pos:#s
hole_#false:#true2_3 :: #false:#true
hole_#EQ:#GT:#LT3_3 :: #EQ:#GT:#LT
hole_:::nil4_3 :: :::nil
gen_#0:#neg:#pos:#s5_3 :: Nat → #0:#neg:#pos:#s
gen_:::nil6_3 :: Nat → :::nil

Lemmas:
#compare(gen_#0:#neg:#pos:#s5_3(n8_3), gen_#0:#neg:#pos:#s5_3(n8_3)) → #EQ, rt ∈ Ω(0)
insertionsortD#1(gen_:::nil6_3(n332039_3)) → *7_3, rt ∈ Ω(n332039₃)
insertionsortD(gen_:::nil6_3(n322968_3)) → *7_3, rt ∈ Ω(n322968₃)

Generator Equations:
gen_#0:#neg:#pos:#s5_3(0) ⇔ #0
gen_#0:#neg:#pos:#s5_3(+(x, 1)) ⇔ #neg(gen_#0:#neg:#pos:#s5_3(x))
gen_:::nil6_3(0) ⇔ nil
gen_:::nil6_3(+(x, 1)) ⇔ ::(#0, gen_:::nil6_3(x))

The following defined symbols remain to be analysed:
insert, insertionsort, insertionsort#1

They will be analysed ascendingly in the following order:
insert = insert#1
insert < insertionsort#1
insertionsort = insertionsort#1

(27) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol insert.

(28) Obligation:

Innermost TRS:
Rules:
#abs(#0) → #0
#abs(#neg(@x)) → #pos(@x)
#abs(#pos(@x)) → #pos(@x)
#abs(#s(@x)) → #pos(#s(@x))
#less(@x, @y) → #cklt(#compare(@x, @y))
insert(@x, @l) → insert#1(@l, @x)
insert#1(::(@y, @ys), @x) → insert#2(#less(@y, @x), @x, @y, @ys)
insert#1(nil, @x) → ::(@x, nil)
insert#2(#false, @x, @y, @ys) → ::(@x, ::(@y, @ys))
insert#2(#true, @x, @y, @ys) → ::(@y, insert(@x, @ys))
insertD(@x, @l) → insertD#1(@l, @x)
insertD#1(::(@y, @ys), @x) → insertD#2(#less(@y, @x), @x, @y, @ys)
insertD#1(nil, @x) → ::(@x, nil)
insertD#2(#false, @x, @y, @ys) → ::(@x, ::(@y, @ys))
insertD#2(#true, @x, @y, @ys) → ::(@y, insertD(@x, @ys))
insertionsort(@l) → insertionsort#1(@l)
insertionsort#1(::(@x, @xs)) → insert(@x, insertionsort(@xs))
insertionsort#1(nil) → nil
insertionsortD(@l) → insertionsortD#1(@l)
insertionsortD#1(::(@x, @xs)) → insertD(@x, insertionsortD(@xs))
insertionsortD#1(nil) → nil
testInsertionsort → insertionsort(testList)
testInsertionsortD → insertionsortD(testList)
testList → ::(#abs(#0), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0))))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#0))))))))), ::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0)))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#0)))))))), ::(#abs(#pos(#s(#s(#s(#0))))), nil))))))))))
#cklt(#EQ) → #false
#cklt(#GT) → #false
#cklt(#LT) → #true
#compare(#0, #0) → #EQ
#compare(#0, #neg(@y)) → #GT
#compare(#0, #pos(@y)) → #LT
#compare(#0, #s(@y)) → #LT
#compare(#neg(@x), #0) → #LT
#compare(#neg(@x), #neg(@y)) → #compare(@y, @x)
#compare(#neg(@x), #pos(@y)) → #LT
#compare(#pos(@x), #0) → #GT
#compare(#pos(@x), #neg(@y)) → #GT
#compare(#pos(@x), #pos(@y)) → #compare(@x, @y)
#compare(#s(@x), #0) → #GT
#compare(#s(@x), #s(@y)) → #compare(@x, @y)

Types:
#abs :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#0 :: #0:#neg:#pos:#s
#neg :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#pos :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#s :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#less :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
#compare :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #EQ:#GT:#LT
insert :: #0:#neg:#pos:#s → :::nil → :::nil
insert#1 :: :::nil → #0:#neg:#pos:#s → :::nil
:: :: #0:#neg:#pos:#s → :::nil → :::nil
insert#2 :: #false:#true → #0:#neg:#pos:#s → #0:#neg:#pos:#s → :::nil → :::nil
nil :: :::nil
#false :: #false:#true
#true :: #false:#true
insertD :: #0:#neg:#pos:#s → :::nil → :::nil
insertD#1 :: :::nil → #0:#neg:#pos:#s → :::nil
insertD#2 :: #false:#true → #0:#neg:#pos:#s → #0:#neg:#pos:#s → :::nil → :::nil
insertionsort :: :::nil → :::nil
insertionsort#1 :: :::nil → :::nil
insertionsortD :: :::nil → :::nil
insertionsortD#1 :: :::nil → :::nil
testInsertionsort :: :::nil
testList :: :::nil
testInsertionsortD :: :::nil
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
hole_#0:#neg:#pos:#s1_3 :: #0:#neg:#pos:#s
hole_#false:#true2_3 :: #false:#true
hole_#EQ:#GT:#LT3_3 :: #EQ:#GT:#LT
hole_:::nil4_3 :: :::nil
gen_#0:#neg:#pos:#s5_3 :: Nat → #0:#neg:#pos:#s
gen_:::nil6_3 :: Nat → :::nil

Lemmas:
#compare(gen_#0:#neg:#pos:#s5_3(n8_3), gen_#0:#neg:#pos:#s5_3(n8_3)) → #EQ, rt ∈ Ω(0)
insertionsortD#1(gen_:::nil6_3(n332039_3)) → *7_3, rt ∈ Ω(n332039₃)
insertionsortD(gen_:::nil6_3(n322968_3)) → *7_3, rt ∈ Ω(n322968₃)

Generator Equations:
gen_#0:#neg:#pos:#s5_3(0) ⇔ #0
gen_#0:#neg:#pos:#s5_3(+(x, 1)) ⇔ #neg(gen_#0:#neg:#pos:#s5_3(x))
gen_:::nil6_3(0) ⇔ nil
gen_:::nil6_3(+(x, 1)) ⇔ ::(#0, gen_:::nil6_3(x))

The following defined symbols remain to be analysed:
insertionsort#1, insertionsort

They will be analysed ascendingly in the following order:
insertionsort = insertionsort#1

(29) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
insertionsort#1(gen_:::nil6_3(n346992_3)) → *7_3, rt ∈ Ω(n346992₃)

Induction Base:
insertionsort#1(gen_:::nil6_3(0))

Induction Step:
insertionsort#1(gen_:::nil6_3(+(n346992_3, 1))) →_R^Ω(1)
insert(#0, insertionsort(gen_:::nil6_3(n346992_3))) →_R^Ω(1)
insert(#0, insertionsort#1(gen_:::nil6_3(n346992_3))) →_IH
insert(#0, *7_3)

We have rt ∈ Ω(n¹) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

(30) Complex Obligation (BEST)

(31) Obligation:

Innermost TRS:
Rules:
#abs(#0) → #0
#abs(#neg(@x)) → #pos(@x)
#abs(#pos(@x)) → #pos(@x)
#abs(#s(@x)) → #pos(#s(@x))
#less(@x, @y) → #cklt(#compare(@x, @y))
insert(@x, @l) → insert#1(@l, @x)
insert#1(::(@y, @ys), @x) → insert#2(#less(@y, @x), @x, @y, @ys)
insert#1(nil, @x) → ::(@x, nil)
insert#2(#false, @x, @y, @ys) → ::(@x, ::(@y, @ys))
insert#2(#true, @x, @y, @ys) → ::(@y, insert(@x, @ys))
insertD(@x, @l) → insertD#1(@l, @x)
insertD#1(::(@y, @ys), @x) → insertD#2(#less(@y, @x), @x, @y, @ys)
insertD#1(nil, @x) → ::(@x, nil)
insertD#2(#false, @x, @y, @ys) → ::(@x, ::(@y, @ys))
insertD#2(#true, @x, @y, @ys) → ::(@y, insertD(@x, @ys))
insertionsort(@l) → insertionsort#1(@l)
insertionsort#1(::(@x, @xs)) → insert(@x, insertionsort(@xs))
insertionsort#1(nil) → nil
insertionsortD(@l) → insertionsortD#1(@l)
insertionsortD#1(::(@x, @xs)) → insertD(@x, insertionsortD(@xs))
insertionsortD#1(nil) → nil
testInsertionsort → insertionsort(testList)
testInsertionsortD → insertionsortD(testList)
testList → ::(#abs(#0), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0))))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#0))))))))), ::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0)))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#0)))))))), ::(#abs(#pos(#s(#s(#s(#0))))), nil))))))))))
#cklt(#EQ) → #false
#cklt(#GT) → #false
#cklt(#LT) → #true
#compare(#0, #0) → #EQ
#compare(#0, #neg(@y)) → #GT
#compare(#0, #pos(@y)) → #LT
#compare(#0, #s(@y)) → #LT
#compare(#neg(@x), #0) → #LT
#compare(#neg(@x), #neg(@y)) → #compare(@y, @x)
#compare(#neg(@x), #pos(@y)) → #LT
#compare(#pos(@x), #0) → #GT
#compare(#pos(@x), #neg(@y)) → #GT
#compare(#pos(@x), #pos(@y)) → #compare(@x, @y)
#compare(#s(@x), #0) → #GT
#compare(#s(@x), #s(@y)) → #compare(@x, @y)

Types:
#abs :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#0 :: #0:#neg:#pos:#s
#neg :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#pos :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#s :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#less :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
#compare :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #EQ:#GT:#LT
insert :: #0:#neg:#pos:#s → :::nil → :::nil
insert#1 :: :::nil → #0:#neg:#pos:#s → :::nil
:: :: #0:#neg:#pos:#s → :::nil → :::nil
insert#2 :: #false:#true → #0:#neg:#pos:#s → #0:#neg:#pos:#s → :::nil → :::nil
nil :: :::nil
#false :: #false:#true
#true :: #false:#true
insertD :: #0:#neg:#pos:#s → :::nil → :::nil
insertD#1 :: :::nil → #0:#neg:#pos:#s → :::nil
insertD#2 :: #false:#true → #0:#neg:#pos:#s → #0:#neg:#pos:#s → :::nil → :::nil
insertionsort :: :::nil → :::nil
insertionsort#1 :: :::nil → :::nil
insertionsortD :: :::nil → :::nil
insertionsortD#1 :: :::nil → :::nil
testInsertionsort :: :::nil
testList :: :::nil
testInsertionsortD :: :::nil
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
hole_#0:#neg:#pos:#s1_3 :: #0:#neg:#pos:#s
hole_#false:#true2_3 :: #false:#true
hole_#EQ:#GT:#LT3_3 :: #EQ:#GT:#LT
hole_:::nil4_3 :: :::nil
gen_#0:#neg:#pos:#s5_3 :: Nat → #0:#neg:#pos:#s
gen_:::nil6_3 :: Nat → :::nil

Lemmas:
#compare(gen_#0:#neg:#pos:#s5_3(n8_3), gen_#0:#neg:#pos:#s5_3(n8_3)) → #EQ, rt ∈ Ω(0)
insertionsortD#1(gen_:::nil6_3(n332039_3)) → *7_3, rt ∈ Ω(n332039₃)
insertionsortD(gen_:::nil6_3(n322968_3)) → *7_3, rt ∈ Ω(n322968₃)
insertionsort#1(gen_:::nil6_3(n346992_3)) → *7_3, rt ∈ Ω(n346992₃)

Generator Equations:
gen_#0:#neg:#pos:#s5_3(0) ⇔ #0
gen_#0:#neg:#pos:#s5_3(+(x, 1)) ⇔ #neg(gen_#0:#neg:#pos:#s5_3(x))
gen_:::nil6_3(0) ⇔ nil
gen_:::nil6_3(+(x, 1)) ⇔ ::(#0, gen_:::nil6_3(x))

The following defined symbols remain to be analysed:
insertionsort

They will be analysed ascendingly in the following order:
insertionsort = insertionsort#1

(32) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
insertionsort(gen_:::nil6_3(n361435_3)) → *7_3, rt ∈ Ω(n361435₃)

Induction Base:
insertionsort(gen_:::nil6_3(0))

Induction Step:
insertionsort(gen_:::nil6_3(+(n361435_3, 1))) →_R^Ω(1)
insertionsort#1(gen_:::nil6_3(+(n361435_3, 1))) →_R^Ω(1)
insert(#0, insertionsort(gen_:::nil6_3(n361435_3))) →_IH
insert(#0, *7_3)

We have rt ∈ Ω(n¹) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

(33) Complex Obligation (BEST)

(34) Obligation:

Innermost TRS:
Rules:
#abs(#0) → #0
#abs(#neg(@x)) → #pos(@x)
#abs(#pos(@x)) → #pos(@x)
#abs(#s(@x)) → #pos(#s(@x))
#less(@x, @y) → #cklt(#compare(@x, @y))
insert(@x, @l) → insert#1(@l, @x)
insert#1(::(@y, @ys), @x) → insert#2(#less(@y, @x), @x, @y, @ys)
insert#1(nil, @x) → ::(@x, nil)
insert#2(#false, @x, @y, @ys) → ::(@x, ::(@y, @ys))
insert#2(#true, @x, @y, @ys) → ::(@y, insert(@x, @ys))
insertD(@x, @l) → insertD#1(@l, @x)
insertD#1(::(@y, @ys), @x) → insertD#2(#less(@y, @x), @x, @y, @ys)
insertD#1(nil, @x) → ::(@x, nil)
insertD#2(#false, @x, @y, @ys) → ::(@x, ::(@y, @ys))
insertD#2(#true, @x, @y, @ys) → ::(@y, insertD(@x, @ys))
insertionsort(@l) → insertionsort#1(@l)
insertionsort#1(::(@x, @xs)) → insert(@x, insertionsort(@xs))
insertionsort#1(nil) → nil
insertionsortD(@l) → insertionsortD#1(@l)
insertionsortD#1(::(@x, @xs)) → insertD(@x, insertionsortD(@xs))
insertionsortD#1(nil) → nil
testInsertionsort → insertionsort(testList)
testInsertionsortD → insertionsortD(testList)
testList → ::(#abs(#0), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0))))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#0))))))))), ::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0)))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#0)))))))), ::(#abs(#pos(#s(#s(#s(#0))))), nil))))))))))
#cklt(#EQ) → #false
#cklt(#GT) → #false
#cklt(#LT) → #true
#compare(#0, #0) → #EQ
#compare(#0, #neg(@y)) → #GT
#compare(#0, #pos(@y)) → #LT
#compare(#0, #s(@y)) → #LT
#compare(#neg(@x), #0) → #LT
#compare(#neg(@x), #neg(@y)) → #compare(@y, @x)
#compare(#neg(@x), #pos(@y)) → #LT
#compare(#pos(@x), #0) → #GT
#compare(#pos(@x), #neg(@y)) → #GT
#compare(#pos(@x), #pos(@y)) → #compare(@x, @y)
#compare(#s(@x), #0) → #GT
#compare(#s(@x), #s(@y)) → #compare(@x, @y)

Types:
#abs :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#0 :: #0:#neg:#pos:#s
#neg :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#pos :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#s :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#less :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
#compare :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #EQ:#GT:#LT
insert :: #0:#neg:#pos:#s → :::nil → :::nil
insert#1 :: :::nil → #0:#neg:#pos:#s → :::nil
:: :: #0:#neg:#pos:#s → :::nil → :::nil
insert#2 :: #false:#true → #0:#neg:#pos:#s → #0:#neg:#pos:#s → :::nil → :::nil
nil :: :::nil
#false :: #false:#true
#true :: #false:#true
insertD :: #0:#neg:#pos:#s → :::nil → :::nil
insertD#1 :: :::nil → #0:#neg:#pos:#s → :::nil
insertD#2 :: #false:#true → #0:#neg:#pos:#s → #0:#neg:#pos:#s → :::nil → :::nil
insertionsort :: :::nil → :::nil
insertionsort#1 :: :::nil → :::nil
insertionsortD :: :::nil → :::nil
insertionsortD#1 :: :::nil → :::nil
testInsertionsort :: :::nil
testList :: :::nil
testInsertionsortD :: :::nil
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
hole_#0:#neg:#pos:#s1_3 :: #0:#neg:#pos:#s
hole_#false:#true2_3 :: #false:#true
hole_#EQ:#GT:#LT3_3 :: #EQ:#GT:#LT
hole_:::nil4_3 :: :::nil
gen_#0:#neg:#pos:#s5_3 :: Nat → #0:#neg:#pos:#s
gen_:::nil6_3 :: Nat → :::nil

Lemmas:
#compare(gen_#0:#neg:#pos:#s5_3(n8_3), gen_#0:#neg:#pos:#s5_3(n8_3)) → #EQ, rt ∈ Ω(0)
insertionsortD#1(gen_:::nil6_3(n332039_3)) → *7_3, rt ∈ Ω(n332039₃)
insertionsortD(gen_:::nil6_3(n322968_3)) → *7_3, rt ∈ Ω(n322968₃)
insertionsort#1(gen_:::nil6_3(n346992_3)) → *7_3, rt ∈ Ω(n346992₃)
insertionsort(gen_:::nil6_3(n361435_3)) → *7_3, rt ∈ Ω(n361435₃)

Generator Equations:
gen_#0:#neg:#pos:#s5_3(0) ⇔ #0
gen_#0:#neg:#pos:#s5_3(+(x, 1)) ⇔ #neg(gen_#0:#neg:#pos:#s5_3(x))
gen_:::nil6_3(0) ⇔ nil
gen_:::nil6_3(+(x, 1)) ⇔ ::(#0, gen_:::nil6_3(x))

The following defined symbols remain to be analysed:
insertionsort#1

They will be analysed ascendingly in the following order:
insertionsort = insertionsort#1

(35) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
insertionsort#1(gen_:::nil6_3(n380696_3)) → *7_3, rt ∈ Ω(n380696₃)

Induction Base:
insertionsort#1(gen_:::nil6_3(0))

Induction Step:
insertionsort#1(gen_:::nil6_3(+(n380696_3, 1))) →_R^Ω(1)
insert(#0, insertionsort(gen_:::nil6_3(n380696_3))) →_R^Ω(1)
insert(#0, insertionsort#1(gen_:::nil6_3(n380696_3))) →_IH
insert(#0, *7_3)

We have rt ∈ Ω(n¹) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

(36) Complex Obligation (BEST)

(37) Obligation:

Innermost TRS:
Rules:
#abs(#0) → #0
#abs(#neg(@x)) → #pos(@x)
#abs(#pos(@x)) → #pos(@x)
#abs(#s(@x)) → #pos(#s(@x))
#less(@x, @y) → #cklt(#compare(@x, @y))
insert(@x, @l) → insert#1(@l, @x)
insert#1(::(@y, @ys), @x) → insert#2(#less(@y, @x), @x, @y, @ys)
insert#1(nil, @x) → ::(@x, nil)
insert#2(#false, @x, @y, @ys) → ::(@x, ::(@y, @ys))
insert#2(#true, @x, @y, @ys) → ::(@y, insert(@x, @ys))
insertD(@x, @l) → insertD#1(@l, @x)
insertD#1(::(@y, @ys), @x) → insertD#2(#less(@y, @x), @x, @y, @ys)
insertD#1(nil, @x) → ::(@x, nil)
insertD#2(#false, @x, @y, @ys) → ::(@x, ::(@y, @ys))
insertD#2(#true, @x, @y, @ys) → ::(@y, insertD(@x, @ys))
insertionsort(@l) → insertionsort#1(@l)
insertionsort#1(::(@x, @xs)) → insert(@x, insertionsort(@xs))
insertionsort#1(nil) → nil
insertionsortD(@l) → insertionsortD#1(@l)
insertionsortD#1(::(@x, @xs)) → insertD(@x, insertionsortD(@xs))
insertionsortD#1(nil) → nil
testInsertionsort → insertionsort(testList)
testInsertionsortD → insertionsortD(testList)
testList → ::(#abs(#0), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0))))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#0))))))))), ::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0)))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#0)))))))), ::(#abs(#pos(#s(#s(#s(#0))))), nil))))))))))
#cklt(#EQ) → #false
#cklt(#GT) → #false
#cklt(#LT) → #true
#compare(#0, #0) → #EQ
#compare(#0, #neg(@y)) → #GT
#compare(#0, #pos(@y)) → #LT
#compare(#0, #s(@y)) → #LT
#compare(#neg(@x), #0) → #LT
#compare(#neg(@x), #neg(@y)) → #compare(@y, @x)
#compare(#neg(@x), #pos(@y)) → #LT
#compare(#pos(@x), #0) → #GT
#compare(#pos(@x), #neg(@y)) → #GT
#compare(#pos(@x), #pos(@y)) → #compare(@x, @y)
#compare(#s(@x), #0) → #GT
#compare(#s(@x), #s(@y)) → #compare(@x, @y)

Types:
#abs :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#0 :: #0:#neg:#pos:#s
#neg :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#pos :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#s :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#less :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
#compare :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #EQ:#GT:#LT
insert :: #0:#neg:#pos:#s → :::nil → :::nil
insert#1 :: :::nil → #0:#neg:#pos:#s → :::nil
:: :: #0:#neg:#pos:#s → :::nil → :::nil
insert#2 :: #false:#true → #0:#neg:#pos:#s → #0:#neg:#pos:#s → :::nil → :::nil
nil :: :::nil
#false :: #false:#true
#true :: #false:#true
insertD :: #0:#neg:#pos:#s → :::nil → :::nil
insertD#1 :: :::nil → #0:#neg:#pos:#s → :::nil
insertD#2 :: #false:#true → #0:#neg:#pos:#s → #0:#neg:#pos:#s → :::nil → :::nil
insertionsort :: :::nil → :::nil
insertionsort#1 :: :::nil → :::nil
insertionsortD :: :::nil → :::nil
insertionsortD#1 :: :::nil → :::nil
testInsertionsort :: :::nil
testList :: :::nil
testInsertionsortD :: :::nil
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
hole_#0:#neg:#pos:#s1_3 :: #0:#neg:#pos:#s
hole_#false:#true2_3 :: #false:#true
hole_#EQ:#GT:#LT3_3 :: #EQ:#GT:#LT
hole_:::nil4_3 :: :::nil
gen_#0:#neg:#pos:#s5_3 :: Nat → #0:#neg:#pos:#s
gen_:::nil6_3 :: Nat → :::nil

Lemmas:
#compare(gen_#0:#neg:#pos:#s5_3(n8_3), gen_#0:#neg:#pos:#s5_3(n8_3)) → #EQ, rt ∈ Ω(0)
insertionsortD#1(gen_:::nil6_3(n332039_3)) → *7_3, rt ∈ Ω(n332039₃)
insertionsortD(gen_:::nil6_3(n322968_3)) → *7_3, rt ∈ Ω(n322968₃)
insertionsort#1(gen_:::nil6_3(n380696_3)) → *7_3, rt ∈ Ω(n380696₃)
insertionsort(gen_:::nil6_3(n361435_3)) → *7_3, rt ∈ Ω(n361435₃)

Generator Equations:
gen_#0:#neg:#pos:#s5_3(0) ⇔ #0
gen_#0:#neg:#pos:#s5_3(+(x, 1)) ⇔ #neg(gen_#0:#neg:#pos:#s5_3(x))
gen_:::nil6_3(0) ⇔ nil
gen_:::nil6_3(+(x, 1)) ⇔ ::(#0, gen_:::nil6_3(x))

No more defined symbols left to analyse.

(38) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
insertionsortD#1(gen_:::nil6_3(n332039_3)) → *7_3, rt ∈ Ω(n332039₃)

(39) BOUNDS(n^1, INF)

(40) Obligation:

Innermost TRS:
Rules:
#abs(#0) → #0
#abs(#neg(@x)) → #pos(@x)
#abs(#pos(@x)) → #pos(@x)
#abs(#s(@x)) → #pos(#s(@x))
#less(@x, @y) → #cklt(#compare(@x, @y))
insert(@x, @l) → insert#1(@l, @x)
insert#1(::(@y, @ys), @x) → insert#2(#less(@y, @x), @x, @y, @ys)
insert#1(nil, @x) → ::(@x, nil)
insert#2(#false, @x, @y, @ys) → ::(@x, ::(@y, @ys))
insert#2(#true, @x, @y, @ys) → ::(@y, insert(@x, @ys))
insertD(@x, @l) → insertD#1(@l, @x)
insertD#1(::(@y, @ys), @x) → insertD#2(#less(@y, @x), @x, @y, @ys)
insertD#1(nil, @x) → ::(@x, nil)
insertD#2(#false, @x, @y, @ys) → ::(@x, ::(@y, @ys))
insertD#2(#true, @x, @y, @ys) → ::(@y, insertD(@x, @ys))
insertionsort(@l) → insertionsort#1(@l)
insertionsort#1(::(@x, @xs)) → insert(@x, insertionsort(@xs))
insertionsort#1(nil) → nil
insertionsortD(@l) → insertionsortD#1(@l)
insertionsortD#1(::(@x, @xs)) → insertD(@x, insertionsortD(@xs))
insertionsortD#1(nil) → nil
testInsertionsort → insertionsort(testList)
testInsertionsortD → insertionsortD(testList)
testList → ::(#abs(#0), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0))))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#0))))))))), ::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0)))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#0)))))))), ::(#abs(#pos(#s(#s(#s(#0))))), nil))))))))))
#cklt(#EQ) → #false
#cklt(#GT) → #false
#cklt(#LT) → #true
#compare(#0, #0) → #EQ
#compare(#0, #neg(@y)) → #GT
#compare(#0, #pos(@y)) → #LT
#compare(#0, #s(@y)) → #LT
#compare(#neg(@x), #0) → #LT
#compare(#neg(@x), #neg(@y)) → #compare(@y, @x)
#compare(#neg(@x), #pos(@y)) → #LT
#compare(#pos(@x), #0) → #GT
#compare(#pos(@x), #neg(@y)) → #GT
#compare(#pos(@x), #pos(@y)) → #compare(@x, @y)
#compare(#s(@x), #0) → #GT
#compare(#s(@x), #s(@y)) → #compare(@x, @y)

Types:
#abs :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#0 :: #0:#neg:#pos:#s
#neg :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#pos :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#s :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#less :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
#compare :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #EQ:#GT:#LT
insert :: #0:#neg:#pos:#s → :::nil → :::nil
insert#1 :: :::nil → #0:#neg:#pos:#s → :::nil
:: :: #0:#neg:#pos:#s → :::nil → :::nil
insert#2 :: #false:#true → #0:#neg:#pos:#s → #0:#neg:#pos:#s → :::nil → :::nil
nil :: :::nil
#false :: #false:#true
#true :: #false:#true
insertD :: #0:#neg:#pos:#s → :::nil → :::nil
insertD#1 :: :::nil → #0:#neg:#pos:#s → :::nil
insertD#2 :: #false:#true → #0:#neg:#pos:#s → #0:#neg:#pos:#s → :::nil → :::nil
insertionsort :: :::nil → :::nil
insertionsort#1 :: :::nil → :::nil
insertionsortD :: :::nil → :::nil
insertionsortD#1 :: :::nil → :::nil
testInsertionsort :: :::nil
testList :: :::nil
testInsertionsortD :: :::nil
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
hole_#0:#neg:#pos:#s1_3 :: #0:#neg:#pos:#s
hole_#false:#true2_3 :: #false:#true
hole_#EQ:#GT:#LT3_3 :: #EQ:#GT:#LT
hole_:::nil4_3 :: :::nil
gen_#0:#neg:#pos:#s5_3 :: Nat → #0:#neg:#pos:#s
gen_:::nil6_3 :: Nat → :::nil

Lemmas:
#compare(gen_#0:#neg:#pos:#s5_3(n8_3), gen_#0:#neg:#pos:#s5_3(n8_3)) → #EQ, rt ∈ Ω(0)
insertionsortD#1(gen_:::nil6_3(n332039_3)) → *7_3, rt ∈ Ω(n332039₃)
insertionsortD(gen_:::nil6_3(n322968_3)) → *7_3, rt ∈ Ω(n322968₃)
insertionsort#1(gen_:::nil6_3(n380696_3)) → *7_3, rt ∈ Ω(n380696₃)
insertionsort(gen_:::nil6_3(n361435_3)) → *7_3, rt ∈ Ω(n361435₃)

Generator Equations:
gen_#0:#neg:#pos:#s5_3(0) ⇔ #0
gen_#0:#neg:#pos:#s5_3(+(x, 1)) ⇔ #neg(gen_#0:#neg:#pos:#s5_3(x))
gen_:::nil6_3(0) ⇔ nil
gen_:::nil6_3(+(x, 1)) ⇔ ::(#0, gen_:::nil6_3(x))

No more defined symbols left to analyse.

(41) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
insertionsortD#1(gen_:::nil6_3(n332039_3)) → *7_3, rt ∈ Ω(n332039₃)

(42) BOUNDS(n^1, INF)

(43) Obligation:

Innermost TRS:
Rules:
#abs(#0) → #0
#abs(#neg(@x)) → #pos(@x)
#abs(#pos(@x)) → #pos(@x)
#abs(#s(@x)) → #pos(#s(@x))
#less(@x, @y) → #cklt(#compare(@x, @y))
insert(@x, @l) → insert#1(@l, @x)
insert#1(::(@y, @ys), @x) → insert#2(#less(@y, @x), @x, @y, @ys)
insert#1(nil, @x) → ::(@x, nil)
insert#2(#false, @x, @y, @ys) → ::(@x, ::(@y, @ys))
insert#2(#true, @x, @y, @ys) → ::(@y, insert(@x, @ys))
insertD(@x, @l) → insertD#1(@l, @x)
insertD#1(::(@y, @ys), @x) → insertD#2(#less(@y, @x), @x, @y, @ys)
insertD#1(nil, @x) → ::(@x, nil)
insertD#2(#false, @x, @y, @ys) → ::(@x, ::(@y, @ys))
insertD#2(#true, @x, @y, @ys) → ::(@y, insertD(@x, @ys))
insertionsort(@l) → insertionsort#1(@l)
insertionsort#1(::(@x, @xs)) → insert(@x, insertionsort(@xs))
insertionsort#1(nil) → nil
insertionsortD(@l) → insertionsortD#1(@l)
insertionsortD#1(::(@x, @xs)) → insertD(@x, insertionsortD(@xs))
insertionsortD#1(nil) → nil
testInsertionsort → insertionsort(testList)
testInsertionsortD → insertionsortD(testList)
testList → ::(#abs(#0), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0))))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#0))))))))), ::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0)))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#0)))))))), ::(#abs(#pos(#s(#s(#s(#0))))), nil))))))))))
#cklt(#EQ) → #false
#cklt(#GT) → #false
#cklt(#LT) → #true
#compare(#0, #0) → #EQ
#compare(#0, #neg(@y)) → #GT
#compare(#0, #pos(@y)) → #LT
#compare(#0, #s(@y)) → #LT
#compare(#neg(@x), #0) → #LT
#compare(#neg(@x), #neg(@y)) → #compare(@y, @x)
#compare(#neg(@x), #pos(@y)) → #LT
#compare(#pos(@x), #0) → #GT
#compare(#pos(@x), #neg(@y)) → #GT
#compare(#pos(@x), #pos(@y)) → #compare(@x, @y)
#compare(#s(@x), #0) → #GT
#compare(#s(@x), #s(@y)) → #compare(@x, @y)

Types:
#abs :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#0 :: #0:#neg:#pos:#s
#neg :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#pos :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#s :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#less :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
#compare :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #EQ:#GT:#LT
insert :: #0:#neg:#pos:#s → :::nil → :::nil
insert#1 :: :::nil → #0:#neg:#pos:#s → :::nil
:: :: #0:#neg:#pos:#s → :::nil → :::nil
insert#2 :: #false:#true → #0:#neg:#pos:#s → #0:#neg:#pos:#s → :::nil → :::nil
nil :: :::nil
#false :: #false:#true
#true :: #false:#true
insertD :: #0:#neg:#pos:#s → :::nil → :::nil
insertD#1 :: :::nil → #0:#neg:#pos:#s → :::nil
insertD#2 :: #false:#true → #0:#neg:#pos:#s → #0:#neg:#pos:#s → :::nil → :::nil
insertionsort :: :::nil → :::nil
insertionsort#1 :: :::nil → :::nil
insertionsortD :: :::nil → :::nil
insertionsortD#1 :: :::nil → :::nil
testInsertionsort :: :::nil
testList :: :::nil
testInsertionsortD :: :::nil
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
hole_#0:#neg:#pos:#s1_3 :: #0:#neg:#pos:#s
hole_#false:#true2_3 :: #false:#true
hole_#EQ:#GT:#LT3_3 :: #EQ:#GT:#LT
hole_:::nil4_3 :: :::nil
gen_#0:#neg:#pos:#s5_3 :: Nat → #0:#neg:#pos:#s
gen_:::nil6_3 :: Nat → :::nil

Lemmas:
#compare(gen_#0:#neg:#pos:#s5_3(n8_3), gen_#0:#neg:#pos:#s5_3(n8_3)) → #EQ, rt ∈ Ω(0)
insertionsortD#1(gen_:::nil6_3(n332039_3)) → *7_3, rt ∈ Ω(n332039₃)
insertionsortD(gen_:::nil6_3(n322968_3)) → *7_3, rt ∈ Ω(n322968₃)
insertionsort#1(gen_:::nil6_3(n346992_3)) → *7_3, rt ∈ Ω(n346992₃)
insertionsort(gen_:::nil6_3(n361435_3)) → *7_3, rt ∈ Ω(n361435₃)

Generator Equations:
gen_#0:#neg:#pos:#s5_3(0) ⇔ #0
gen_#0:#neg:#pos:#s5_3(+(x, 1)) ⇔ #neg(gen_#0:#neg:#pos:#s5_3(x))
gen_:::nil6_3(0) ⇔ nil
gen_:::nil6_3(+(x, 1)) ⇔ ::(#0, gen_:::nil6_3(x))

No more defined symbols left to analyse.

(44) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
insertionsortD#1(gen_:::nil6_3(n332039_3)) → *7_3, rt ∈ Ω(n332039₃)

(45) BOUNDS(n^1, INF)

(46) Obligation:

Innermost TRS:
Rules:
#abs(#0) → #0
#abs(#neg(@x)) → #pos(@x)
#abs(#pos(@x)) → #pos(@x)
#abs(#s(@x)) → #pos(#s(@x))
#less(@x, @y) → #cklt(#compare(@x, @y))
insert(@x, @l) → insert#1(@l, @x)
insert#1(::(@y, @ys), @x) → insert#2(#less(@y, @x), @x, @y, @ys)
insert#1(nil, @x) → ::(@x, nil)
insert#2(#false, @x, @y, @ys) → ::(@x, ::(@y, @ys))
insert#2(#true, @x, @y, @ys) → ::(@y, insert(@x, @ys))
insertD(@x, @l) → insertD#1(@l, @x)
insertD#1(::(@y, @ys), @x) → insertD#2(#less(@y, @x), @x, @y, @ys)
insertD#1(nil, @x) → ::(@x, nil)
insertD#2(#false, @x, @y, @ys) → ::(@x, ::(@y, @ys))
insertD#2(#true, @x, @y, @ys) → ::(@y, insertD(@x, @ys))
insertionsort(@l) → insertionsort#1(@l)
insertionsort#1(::(@x, @xs)) → insert(@x, insertionsort(@xs))
insertionsort#1(nil) → nil
insertionsortD(@l) → insertionsortD#1(@l)
insertionsortD#1(::(@x, @xs)) → insertD(@x, insertionsortD(@xs))
insertionsortD#1(nil) → nil
testInsertionsort → insertionsort(testList)
testInsertionsortD → insertionsortD(testList)
testList → ::(#abs(#0), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0))))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#0))))))))), ::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0)))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#0)))))))), ::(#abs(#pos(#s(#s(#s(#0))))), nil))))))))))
#cklt(#EQ) → #false
#cklt(#GT) → #false
#cklt(#LT) → #true
#compare(#0, #0) → #EQ
#compare(#0, #neg(@y)) → #GT
#compare(#0, #pos(@y)) → #LT
#compare(#0, #s(@y)) → #LT
#compare(#neg(@x), #0) → #LT
#compare(#neg(@x), #neg(@y)) → #compare(@y, @x)
#compare(#neg(@x), #pos(@y)) → #LT
#compare(#pos(@x), #0) → #GT
#compare(#pos(@x), #neg(@y)) → #GT
#compare(#pos(@x), #pos(@y)) → #compare(@x, @y)
#compare(#s(@x), #0) → #GT
#compare(#s(@x), #s(@y)) → #compare(@x, @y)

Types:
#abs :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#0 :: #0:#neg:#pos:#s
#neg :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#pos :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#s :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#less :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
#compare :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #EQ:#GT:#LT
insert :: #0:#neg:#pos:#s → :::nil → :::nil
insert#1 :: :::nil → #0:#neg:#pos:#s → :::nil
:: :: #0:#neg:#pos:#s → :::nil → :::nil
insert#2 :: #false:#true → #0:#neg:#pos:#s → #0:#neg:#pos:#s → :::nil → :::nil
nil :: :::nil
#false :: #false:#true
#true :: #false:#true
insertD :: #0:#neg:#pos:#s → :::nil → :::nil
insertD#1 :: :::nil → #0:#neg:#pos:#s → :::nil
insertD#2 :: #false:#true → #0:#neg:#pos:#s → #0:#neg:#pos:#s → :::nil → :::nil
insertionsort :: :::nil → :::nil
insertionsort#1 :: :::nil → :::nil
insertionsortD :: :::nil → :::nil
insertionsortD#1 :: :::nil → :::nil
testInsertionsort :: :::nil
testList :: :::nil
testInsertionsortD :: :::nil
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
hole_#0:#neg:#pos:#s1_3 :: #0:#neg:#pos:#s
hole_#false:#true2_3 :: #false:#true
hole_#EQ:#GT:#LT3_3 :: #EQ:#GT:#LT
hole_:::nil4_3 :: :::nil
gen_#0:#neg:#pos:#s5_3 :: Nat → #0:#neg:#pos:#s
gen_:::nil6_3 :: Nat → :::nil

Lemmas:
#compare(gen_#0:#neg:#pos:#s5_3(n8_3), gen_#0:#neg:#pos:#s5_3(n8_3)) → #EQ, rt ∈ Ω(0)
insertionsortD#1(gen_:::nil6_3(n332039_3)) → *7_3, rt ∈ Ω(n332039₃)
insertionsortD(gen_:::nil6_3(n322968_3)) → *7_3, rt ∈ Ω(n322968₃)
insertionsort#1(gen_:::nil6_3(n346992_3)) → *7_3, rt ∈ Ω(n346992₃)

Generator Equations:
gen_#0:#neg:#pos:#s5_3(0) ⇔ #0
gen_#0:#neg:#pos:#s5_3(+(x, 1)) ⇔ #neg(gen_#0:#neg:#pos:#s5_3(x))
gen_:::nil6_3(0) ⇔ nil
gen_:::nil6_3(+(x, 1)) ⇔ ::(#0, gen_:::nil6_3(x))

No more defined symbols left to analyse.

(47) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
insertionsortD#1(gen_:::nil6_3(n332039_3)) → *7_3, rt ∈ Ω(n332039₃)

(48) BOUNDS(n^1, INF)

(49) Obligation:

Innermost TRS:
Rules:
#abs(#0) → #0
#abs(#neg(@x)) → #pos(@x)
#abs(#pos(@x)) → #pos(@x)
#abs(#s(@x)) → #pos(#s(@x))
#less(@x, @y) → #cklt(#compare(@x, @y))
insert(@x, @l) → insert#1(@l, @x)
insert#1(::(@y, @ys), @x) → insert#2(#less(@y, @x), @x, @y, @ys)
insert#1(nil, @x) → ::(@x, nil)
insert#2(#false, @x, @y, @ys) → ::(@x, ::(@y, @ys))
insert#2(#true, @x, @y, @ys) → ::(@y, insert(@x, @ys))
insertD(@x, @l) → insertD#1(@l, @x)
insertD#1(::(@y, @ys), @x) → insertD#2(#less(@y, @x), @x, @y, @ys)
insertD#1(nil, @x) → ::(@x, nil)
insertD#2(#false, @x, @y, @ys) → ::(@x, ::(@y, @ys))
insertD#2(#true, @x, @y, @ys) → ::(@y, insertD(@x, @ys))
insertionsort(@l) → insertionsort#1(@l)
insertionsort#1(::(@x, @xs)) → insert(@x, insertionsort(@xs))
insertionsort#1(nil) → nil
insertionsortD(@l) → insertionsortD#1(@l)
insertionsortD#1(::(@x, @xs)) → insertD(@x, insertionsortD(@xs))
insertionsortD#1(nil) → nil
testInsertionsort → insertionsort(testList)
testInsertionsortD → insertionsortD(testList)
testList → ::(#abs(#0), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0))))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#0))))))))), ::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0)))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#0)))))))), ::(#abs(#pos(#s(#s(#s(#0))))), nil))))))))))
#cklt(#EQ) → #false
#cklt(#GT) → #false
#cklt(#LT) → #true
#compare(#0, #0) → #EQ
#compare(#0, #neg(@y)) → #GT
#compare(#0, #pos(@y)) → #LT
#compare(#0, #s(@y)) → #LT
#compare(#neg(@x), #0) → #LT
#compare(#neg(@x), #neg(@y)) → #compare(@y, @x)
#compare(#neg(@x), #pos(@y)) → #LT
#compare(#pos(@x), #0) → #GT
#compare(#pos(@x), #neg(@y)) → #GT
#compare(#pos(@x), #pos(@y)) → #compare(@x, @y)
#compare(#s(@x), #0) → #GT
#compare(#s(@x), #s(@y)) → #compare(@x, @y)

Types:
#abs :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#0 :: #0:#neg:#pos:#s
#neg :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#pos :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#s :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#less :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
#compare :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #EQ:#GT:#LT
insert :: #0:#neg:#pos:#s → :::nil → :::nil
insert#1 :: :::nil → #0:#neg:#pos:#s → :::nil
:: :: #0:#neg:#pos:#s → :::nil → :::nil
insert#2 :: #false:#true → #0:#neg:#pos:#s → #0:#neg:#pos:#s → :::nil → :::nil
nil :: :::nil
#false :: #false:#true
#true :: #false:#true
insertD :: #0:#neg:#pos:#s → :::nil → :::nil
insertD#1 :: :::nil → #0:#neg:#pos:#s → :::nil
insertD#2 :: #false:#true → #0:#neg:#pos:#s → #0:#neg:#pos:#s → :::nil → :::nil
insertionsort :: :::nil → :::nil
insertionsort#1 :: :::nil → :::nil
insertionsortD :: :::nil → :::nil
insertionsortD#1 :: :::nil → :::nil
testInsertionsort :: :::nil
testList :: :::nil
testInsertionsortD :: :::nil
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
hole_#0:#neg:#pos:#s1_3 :: #0:#neg:#pos:#s
hole_#false:#true2_3 :: #false:#true
hole_#EQ:#GT:#LT3_3 :: #EQ:#GT:#LT
hole_:::nil4_3 :: :::nil
gen_#0:#neg:#pos:#s5_3 :: Nat → #0:#neg:#pos:#s
gen_:::nil6_3 :: Nat → :::nil

Lemmas:
#compare(gen_#0:#neg:#pos:#s5_3(n8_3), gen_#0:#neg:#pos:#s5_3(n8_3)) → #EQ, rt ∈ Ω(0)
insertionsortD#1(gen_:::nil6_3(n332039_3)) → *7_3, rt ∈ Ω(n332039₃)
insertionsortD(gen_:::nil6_3(n322968_3)) → *7_3, rt ∈ Ω(n322968₃)

Generator Equations:
gen_#0:#neg:#pos:#s5_3(0) ⇔ #0
gen_#0:#neg:#pos:#s5_3(+(x, 1)) ⇔ #neg(gen_#0:#neg:#pos:#s5_3(x))
gen_:::nil6_3(0) ⇔ nil
gen_:::nil6_3(+(x, 1)) ⇔ ::(#0, gen_:::nil6_3(x))

No more defined symbols left to analyse.

(50) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
insertionsortD#1(gen_:::nil6_3(n332039_3)) → *7_3, rt ∈ Ω(n332039₃)

(51) BOUNDS(n^1, INF)

(52) Obligation:

Innermost TRS:
Rules:
#abs(#0) → #0
#abs(#neg(@x)) → #pos(@x)
#abs(#pos(@x)) → #pos(@x)
#abs(#s(@x)) → #pos(#s(@x))
#less(@x, @y) → #cklt(#compare(@x, @y))
insert(@x, @l) → insert#1(@l, @x)
insert#1(::(@y, @ys), @x) → insert#2(#less(@y, @x), @x, @y, @ys)
insert#1(nil, @x) → ::(@x, nil)
insert#2(#false, @x, @y, @ys) → ::(@x, ::(@y, @ys))
insert#2(#true, @x, @y, @ys) → ::(@y, insert(@x, @ys))
insertD(@x, @l) → insertD#1(@l, @x)
insertD#1(::(@y, @ys), @x) → insertD#2(#less(@y, @x), @x, @y, @ys)
insertD#1(nil, @x) → ::(@x, nil)
insertD#2(#false, @x, @y, @ys) → ::(@x, ::(@y, @ys))
insertD#2(#true, @x, @y, @ys) → ::(@y, insertD(@x, @ys))
insertionsort(@l) → insertionsort#1(@l)
insertionsort#1(::(@x, @xs)) → insert(@x, insertionsort(@xs))
insertionsort#1(nil) → nil
insertionsortD(@l) → insertionsortD#1(@l)
insertionsortD#1(::(@x, @xs)) → insertD(@x, insertionsortD(@xs))
insertionsortD#1(nil) → nil
testInsertionsort → insertionsort(testList)
testInsertionsortD → insertionsortD(testList)
testList → ::(#abs(#0), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0))))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#0))))))))), ::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0)))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#0)))))))), ::(#abs(#pos(#s(#s(#s(#0))))), nil))))))))))
#cklt(#EQ) → #false
#cklt(#GT) → #false
#cklt(#LT) → #true
#compare(#0, #0) → #EQ
#compare(#0, #neg(@y)) → #GT
#compare(#0, #pos(@y)) → #LT
#compare(#0, #s(@y)) → #LT
#compare(#neg(@x), #0) → #LT
#compare(#neg(@x), #neg(@y)) → #compare(@y, @x)
#compare(#neg(@x), #pos(@y)) → #LT
#compare(#pos(@x), #0) → #GT
#compare(#pos(@x), #neg(@y)) → #GT
#compare(#pos(@x), #pos(@y)) → #compare(@x, @y)
#compare(#s(@x), #0) → #GT
#compare(#s(@x), #s(@y)) → #compare(@x, @y)

Types:
#abs :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#0 :: #0:#neg:#pos:#s
#neg :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#pos :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#s :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#less :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
#compare :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #EQ:#GT:#LT
insert :: #0:#neg:#pos:#s → :::nil → :::nil
insert#1 :: :::nil → #0:#neg:#pos:#s → :::nil
:: :: #0:#neg:#pos:#s → :::nil → :::nil
insert#2 :: #false:#true → #0:#neg:#pos:#s → #0:#neg:#pos:#s → :::nil → :::nil
nil :: :::nil
#false :: #false:#true
#true :: #false:#true
insertD :: #0:#neg:#pos:#s → :::nil → :::nil
insertD#1 :: :::nil → #0:#neg:#pos:#s → :::nil
insertD#2 :: #false:#true → #0:#neg:#pos:#s → #0:#neg:#pos:#s → :::nil → :::nil
insertionsort :: :::nil → :::nil
insertionsort#1 :: :::nil → :::nil
insertionsortD :: :::nil → :::nil
insertionsortD#1 :: :::nil → :::nil
testInsertionsort :: :::nil
testList :: :::nil
testInsertionsortD :: :::nil
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
hole_#0:#neg:#pos:#s1_3 :: #0:#neg:#pos:#s
hole_#false:#true2_3 :: #false:#true
hole_#EQ:#GT:#LT3_3 :: #EQ:#GT:#LT
hole_:::nil4_3 :: :::nil
gen_#0:#neg:#pos:#s5_3 :: Nat → #0:#neg:#pos:#s
gen_:::nil6_3 :: Nat → :::nil

Lemmas:
#compare(gen_#0:#neg:#pos:#s5_3(n8_3), gen_#0:#neg:#pos:#s5_3(n8_3)) → #EQ, rt ∈ Ω(0)
insertionsortD#1(gen_:::nil6_3(n319337_3)) → *7_3, rt ∈ Ω(n319337₃)
insertionsortD(gen_:::nil6_3(n322968_3)) → *7_3, rt ∈ Ω(n322968₃)

Generator Equations:
gen_#0:#neg:#pos:#s5_3(0) ⇔ #0
gen_#0:#neg:#pos:#s5_3(+(x, 1)) ⇔ #neg(gen_#0:#neg:#pos:#s5_3(x))
gen_:::nil6_3(0) ⇔ nil
gen_:::nil6_3(+(x, 1)) ⇔ ::(#0, gen_:::nil6_3(x))

No more defined symbols left to analyse.

(53) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
insertionsortD#1(gen_:::nil6_3(n319337_3)) → *7_3, rt ∈ Ω(n319337₃)

(54) BOUNDS(n^1, INF)

(55) Obligation:

Innermost TRS:
Rules:
#abs(#0) → #0
#abs(#neg(@x)) → #pos(@x)
#abs(#pos(@x)) → #pos(@x)
#abs(#s(@x)) → #pos(#s(@x))
#less(@x, @y) → #cklt(#compare(@x, @y))
insert(@x, @l) → insert#1(@l, @x)
insert#1(::(@y, @ys), @x) → insert#2(#less(@y, @x), @x, @y, @ys)
insert#1(nil, @x) → ::(@x, nil)
insert#2(#false, @x, @y, @ys) → ::(@x, ::(@y, @ys))
insert#2(#true, @x, @y, @ys) → ::(@y, insert(@x, @ys))
insertD(@x, @l) → insertD#1(@l, @x)
insertD#1(::(@y, @ys), @x) → insertD#2(#less(@y, @x), @x, @y, @ys)
insertD#1(nil, @x) → ::(@x, nil)
insertD#2(#false, @x, @y, @ys) → ::(@x, ::(@y, @ys))
insertD#2(#true, @x, @y, @ys) → ::(@y, insertD(@x, @ys))
insertionsort(@l) → insertionsort#1(@l)
insertionsort#1(::(@x, @xs)) → insert(@x, insertionsort(@xs))
insertionsort#1(nil) → nil
insertionsortD(@l) → insertionsortD#1(@l)
insertionsortD#1(::(@x, @xs)) → insertD(@x, insertionsortD(@xs))
insertionsortD#1(nil) → nil
testInsertionsort → insertionsort(testList)
testInsertionsortD → insertionsortD(testList)
testList → ::(#abs(#0), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0))))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#0))))))))), ::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0)))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#0)))))))), ::(#abs(#pos(#s(#s(#s(#0))))), nil))))))))))
#cklt(#EQ) → #false
#cklt(#GT) → #false
#cklt(#LT) → #true
#compare(#0, #0) → #EQ
#compare(#0, #neg(@y)) → #GT
#compare(#0, #pos(@y)) → #LT
#compare(#0, #s(@y)) → #LT
#compare(#neg(@x), #0) → #LT
#compare(#neg(@x), #neg(@y)) → #compare(@y, @x)
#compare(#neg(@x), #pos(@y)) → #LT
#compare(#pos(@x), #0) → #GT
#compare(#pos(@x), #neg(@y)) → #GT
#compare(#pos(@x), #pos(@y)) → #compare(@x, @y)
#compare(#s(@x), #0) → #GT
#compare(#s(@x), #s(@y)) → #compare(@x, @y)

Types:
#abs :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#0 :: #0:#neg:#pos:#s
#neg :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#pos :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#s :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#less :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
#compare :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #EQ:#GT:#LT
insert :: #0:#neg:#pos:#s → :::nil → :::nil
insert#1 :: :::nil → #0:#neg:#pos:#s → :::nil
:: :: #0:#neg:#pos:#s → :::nil → :::nil
insert#2 :: #false:#true → #0:#neg:#pos:#s → #0:#neg:#pos:#s → :::nil → :::nil
nil :: :::nil
#false :: #false:#true
#true :: #false:#true
insertD :: #0:#neg:#pos:#s → :::nil → :::nil
insertD#1 :: :::nil → #0:#neg:#pos:#s → :::nil
insertD#2 :: #false:#true → #0:#neg:#pos:#s → #0:#neg:#pos:#s → :::nil → :::nil
insertionsort :: :::nil → :::nil
insertionsort#1 :: :::nil → :::nil
insertionsortD :: :::nil → :::nil
insertionsortD#1 :: :::nil → :::nil
testInsertionsort :: :::nil
testList :: :::nil
testInsertionsortD :: :::nil
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
hole_#0:#neg:#pos:#s1_3 :: #0:#neg:#pos:#s
hole_#false:#true2_3 :: #false:#true
hole_#EQ:#GT:#LT3_3 :: #EQ:#GT:#LT
hole_:::nil4_3 :: :::nil
gen_#0:#neg:#pos:#s5_3 :: Nat → #0:#neg:#pos:#s
gen_:::nil6_3 :: Nat → :::nil

Lemmas:
#compare(gen_#0:#neg:#pos:#s5_3(n8_3), gen_#0:#neg:#pos:#s5_3(n8_3)) → #EQ, rt ∈ Ω(0)
insertionsortD#1(gen_:::nil6_3(n319337_3)) → *7_3, rt ∈ Ω(n319337₃)

Generator Equations:
gen_#0:#neg:#pos:#s5_3(0) ⇔ #0
gen_#0:#neg:#pos:#s5_3(+(x, 1)) ⇔ #neg(gen_#0:#neg:#pos:#s5_3(x))
gen_:::nil6_3(0) ⇔ nil
gen_:::nil6_3(+(x, 1)) ⇔ ::(#0, gen_:::nil6_3(x))

No more defined symbols left to analyse.

(56) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
insertionsortD#1(gen_:::nil6_3(n319337_3)) → *7_3, rt ∈ Ω(n319337₃)

(57) BOUNDS(n^1, INF)

(58) Obligation:

Innermost TRS:
Rules:
#abs(#0) → #0
#abs(#neg(@x)) → #pos(@x)
#abs(#pos(@x)) → #pos(@x)
#abs(#s(@x)) → #pos(#s(@x))
#less(@x, @y) → #cklt(#compare(@x, @y))
insert(@x, @l) → insert#1(@l, @x)
insert#1(::(@y, @ys), @x) → insert#2(#less(@y, @x), @x, @y, @ys)
insert#1(nil, @x) → ::(@x, nil)
insert#2(#false, @x, @y, @ys) → ::(@x, ::(@y, @ys))
insert#2(#true, @x, @y, @ys) → ::(@y, insert(@x, @ys))
insertD(@x, @l) → insertD#1(@l, @x)
insertD#1(::(@y, @ys), @x) → insertD#2(#less(@y, @x), @x, @y, @ys)
insertD#1(nil, @x) → ::(@x, nil)
insertD#2(#false, @x, @y, @ys) → ::(@x, ::(@y, @ys))
insertD#2(#true, @x, @y, @ys) → ::(@y, insertD(@x, @ys))
insertionsort(@l) → insertionsort#1(@l)
insertionsort#1(::(@x, @xs)) → insert(@x, insertionsort(@xs))
insertionsort#1(nil) → nil
insertionsortD(@l) → insertionsortD#1(@l)
insertionsortD#1(::(@x, @xs)) → insertD(@x, insertionsortD(@xs))
insertionsortD#1(nil) → nil
testInsertionsort → insertionsort(testList)
testInsertionsortD → insertionsortD(testList)
testList → ::(#abs(#0), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0))))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#0))))))))), ::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0)))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#0)))))))), ::(#abs(#pos(#s(#s(#s(#0))))), nil))))))))))
#cklt(#EQ) → #false
#cklt(#GT) → #false
#cklt(#LT) → #true
#compare(#0, #0) → #EQ
#compare(#0, #neg(@y)) → #GT
#compare(#0, #pos(@y)) → #LT
#compare(#0, #s(@y)) → #LT
#compare(#neg(@x), #0) → #LT
#compare(#neg(@x), #neg(@y)) → #compare(@y, @x)
#compare(#neg(@x), #pos(@y)) → #LT
#compare(#pos(@x), #0) → #GT
#compare(#pos(@x), #neg(@y)) → #GT
#compare(#pos(@x), #pos(@y)) → #compare(@x, @y)
#compare(#s(@x), #0) → #GT
#compare(#s(@x), #s(@y)) → #compare(@x, @y)

Types:
#abs :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#0 :: #0:#neg:#pos:#s
#neg :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#pos :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#s :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#less :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
#compare :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #EQ:#GT:#LT
insert :: #0:#neg:#pos:#s → :::nil → :::nil
insert#1 :: :::nil → #0:#neg:#pos:#s → :::nil
:: :: #0:#neg:#pos:#s → :::nil → :::nil
insert#2 :: #false:#true → #0:#neg:#pos:#s → #0:#neg:#pos:#s → :::nil → :::nil
nil :: :::nil
#false :: #false:#true
#true :: #false:#true
insertD :: #0:#neg:#pos:#s → :::nil → :::nil
insertD#1 :: :::nil → #0:#neg:#pos:#s → :::nil
insertD#2 :: #false:#true → #0:#neg:#pos:#s → #0:#neg:#pos:#s → :::nil → :::nil
insertionsort :: :::nil → :::nil
insertionsort#1 :: :::nil → :::nil
insertionsortD :: :::nil → :::nil
insertionsortD#1 :: :::nil → :::nil
testInsertionsort :: :::nil
testList :: :::nil
testInsertionsortD :: :::nil
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
hole_#0:#neg:#pos:#s1_3 :: #0:#neg:#pos:#s
hole_#false:#true2_3 :: #false:#true
hole_#EQ:#GT:#LT3_3 :: #EQ:#GT:#LT
hole_:::nil4_3 :: :::nil
gen_#0:#neg:#pos:#s5_3 :: Nat → #0:#neg:#pos:#s
gen_:::nil6_3 :: Nat → :::nil

Lemmas:
#compare(gen_#0:#neg:#pos:#s5_3(n8_3), gen_#0:#neg:#pos:#s5_3(n8_3)) → #EQ, rt ∈ Ω(0)

Generator Equations:
gen_#0:#neg:#pos:#s5_3(0) ⇔ #0
gen_#0:#neg:#pos:#s5_3(+(x, 1)) ⇔ #neg(gen_#0:#neg:#pos:#s5_3(x))
gen_:::nil6_3(0) ⇔ nil
gen_:::nil6_3(+(x, 1)) ⇔ ::(#0, gen_:::nil6_3(x))

No more defined symbols left to analyse.

(59) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(1) was proven with the following lemma:
#compare(gen_#0:#neg:#pos:#s5_3(n8_3), gen_#0:#neg:#pos:#s5_3(n8_3)) → #EQ, rt ∈ Ω(0)

(60) BOUNDS(1, INF)